unitsEquivUnitsType — Mathlib

English

There is a natural equivalence between the subgroup of units of S and the units of S.

Русский

Существует естественное эквивалентность между подгруппой единиц S и единицами S.

LaTeX

$$$ S.units \cong_* S^{\times} $$$

Lean4

/-- The equivalence between the subgroup of units of `S` and the type of units of `S`. -/
@[to_additive /-- The equivalence between the additive subgroup of additive units of
    `S` and the type of additive units of `S`. -/
    ]
def unitsEquivUnitsType (S : Submonoid M) : S.units ≃* Sˣ
    where
  toFun := fun ⟨_, h⟩ => ⟨⟨_, h.1⟩, ⟨_, h.2⟩, S.mk_mul_mk_inv_eq_one h, S.mk_inv_mul_mk_eq_one h⟩
  invFun := fun x => ⟨⟨_, _, S.coe_val_mul_coe_inv_val, S.coe_inv_val_mul_coe_val⟩, ⟨x.1.2, x.2.2⟩⟩
  map_mul' := fun _ _ => rfl

Похожие утверждения