# 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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

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 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
@[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 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_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_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 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 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
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)