torsionMulEquiv_apply — Mathlib

English

The torsion isomorphism evaluated at an element a of the torsion submonoid equals the image of a under the corresponding submonoid congruence to the ambient monoid.

Русский

Обратное отображение изоморфизма торсионности, примененное к элементу a из торсионной подмоноиды, равно образу a по соответствующему конгруентному отображению подмоноидов в окружном моноиде.

LaTeX

$$$t_G. torsionMulEquiv(a) = MulEquiv.submonoidCongr(t_G.torsion\_eq\_top)(a).$$$

Lean4

@[to_additive]
theorem torsionMulEquiv_apply (tG : IsTorsion G) (a : torsion G) :
    tG.torsionMulEquiv a = MulEquiv.submonoidCongr tG.torsion_eq_top a :=
  rfl

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