torsionMapQuot_apply — Mathlib

English

For any unit x in the torsion subgroup, the torsion map quotient evaluated at x corresponds to the quotient map: it sends x to the class of x modulo I.

Русский

Для любого элемента-разветвления из torsion отображение torsionMapQuot применимо к x и даёт класс x в фактор-модуле I.

LaTeX

$$$\\operatorname{torsionMapQuot}(I)(\\langle x, \\! x\\in\\mathrm{torsion} K\\rangle) = \\mathrm{Ideal}.Quotient.mk(I)\\, x$$$

Lean4

@[simp]
theorem torsionMapQuot_apply {x : (𝓞 K)ˣ} (hx : x ∈ torsion K) : torsionMapQuot I ⟨x, hx⟩ = Ideal.Quotient.mk I x :=
  rfl

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