mulEquiv_units — Mathlib

English

There is a nonempty MulChar M R ≃* Mˣ, i.e., a monoid equivalence between characters and units.

Русский

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

LaTeX

$$Nonempty (MulChar M R ≃* Mˣ)$$

Lean4

/-- The group of `R`-valued multiplicative characters on a finite commutative monoid `M` is
(noncanonically) isomorphic to its unit group `Mˣ` when `R` is a ring that has enough roots
of unity. -/
theorem mulEquiv_units : Nonempty (MulChar M R ≃* Mˣ) :=
  ⟨mulEquivToUnitHom.trans (CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity Mˣ R).some⟩

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