Documentation

Mathlib.Algebra.Group.Pi.Units

Units in pi types #

source
🔸 coverage
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.

Instances For
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      @[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
      📐 coverage
      @[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
      📐 coverage
      @[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
      📐 coverage
      @[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
      📐 coverage
      @[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
      📐 coverage
      @[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
      📐 coverage
      @[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
      📐 coverage
      @[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
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      instance Pi.instSubsingletonUnits {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] [∀ (i : ι), Subsingleton (M i)ˣ] :
      Subsingleton ((i : ι) → M i)ˣ
      source
      📐 coverage
      instance Pi.instSubsingletonAddUnits {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] [∀ (i : ι), Subsingleton (AddUnits (M i))] :
      Subsingleton (AddUnits ((i : ι) → M i))
      source
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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)