Documentation

Mathlib.Algebra.Group.Pi.Units

Units in pi types #

source
def MulEquiv.piUnits {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] :
((i : ι) → M i)ˣ ≃* ((i : ι) → (M i)ˣ)

The monoid equivalence between units of a product, and the product of the units of each monoid.

Equations
    Instances For
      source
      def AddEquiv.piAddUnits {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] :
      AddUnits ((i : ι) → M i) ≃+ ((i : ι) → AddUnits (M i))

      The additive-monoid equivalence between (additive) units of a product, and the product of the (additive) units of each monoid.

      Equations
        Instances For
          source
          @[simp]
          theorem AddEquiv.val_piAddUnits_symm_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] (f : (i : ι) → AddUnits (M i)) (x✝ : ι) :
          ↑(piAddUnits.symm f) x✝ = ↑(f x✝)
          source
          @[simp]
          theorem AddEquiv.val_piAddUnits_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] (f : AddUnits ((i : ι) → M i)) (i : ι) :
          ↑(piAddUnits f i) = ↑f i
          source
          @[simp]
          theorem MulEquiv.val_piUnits_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] (f : ((i : ι) → M i)ˣ) (i : ι) :
          ↑(piUnits f i) = ↑f i
          source
          @[simp]
          theorem AddEquiv.val_neg_piAddUnits_symm_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] (f : (i : ι) → AddUnits (M i)) (x✝ : ι) :
          ↑(-piAddUnits.symm f) x✝ = (f x✝).neg
          source
          @[simp]
          theorem MulEquiv.val_piUnits_symm_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] (f : (i : ι) → (M i)ˣ) (x✝ : ι) :
          ↑(piUnits.symm f) x✝ = ↑(f x✝)
          source
          @[simp]
          theorem AddEquiv.val_neg_piAddUnits_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] (f : AddUnits ((i : ι) → M i)) (i : ι) :
          ↑(-piAddUnits f i) = f.neg i
          source
          @[simp]
          theorem MulEquiv.val_inv_piUnits_symm_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] (f : (i : ι) → (M i)ˣ) (x✝ : ι) :
          ↑(piUnits.symm f)⁻¹ x✝ = (f x✝).inv
          source
          @[simp]
          theorem MulEquiv.val_inv_piUnits_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] (f : ((i : ι) → M i)ˣ) (i : ι) :
          ↑(piUnits f i)⁻¹ = f.inv i
          source
          theorem Pi.isUnit_iff {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] {x : (i : ι) → M i} :
          IsUnit x ↔ ∀ (i : ι), IsUnit (x i)
          source
          theorem Pi.isAddUnit_iff {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] {x : (i : ι) → M i} :
          IsAddUnit x ↔ ∀ (i : ι), IsAddUnit (x i)
          source
          theorem IsUnit.apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] {x : (i : ι) → M i} :
          IsUnit x → ∀ (i : ι), IsUnit (x i)

          Alias of the forward direction of Pi.isUnit_iff.

          source
          theorem IsAddUnit.apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] {x : (i : ι) → M i} :
          IsAddUnit x → ∀ (i : ι), IsAddUnit (x i)
          source
          theorem IsUnit.val_inv_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] {x : (i : ι) → M i} (hx : IsUnit x) (i : ι) :
          ↑hx.unit⁻¹ i = ↑⋯.unit⁻¹
          source
          theorem IsAddUnit.val_neg_apply {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] {x : (i : ι) → M i} (hx : IsAddUnit x) (i : ι) :
          ↑(-hx.addUnit) i = ↑(-⋯.addUnit)