toUnits_val_apply — Mathlib

English

For every isomorphism h: M ≃* N, the induced map on units mapEquiv h: Mˣ ≃* Nˣ sends a unit x ∈ Mˣ to the corresponding unit h x in Nˣ, and on underlying values it acts by h.

Русский

Для изоморфизма h: M ≃* NR, индуцированное отображение над единицами mapEquiv h: Mˣ ≃* Nˣ переводит единицу x ∈ Mˣ в соответствующую единицу h x в Nˣ, а по значениям действует через h.

LaTeX

$$$\\mathrm{mapEquiv}(h): M^{\\times} \\simeq N^{\\times}$$$

Lean4

@[to_additive (attr := simp)]
theorem toUnits_val_apply {G : Type*} [Group G] (x : Gˣ) : toUnits (x : G) = x := by
  simp_rw [MulEquiv.apply_eq_iff_symm_apply, toUnits_symm_apply]

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