unitsSMulGroup_snd — Mathlib

English

In the previous construction, the second component of the pair produced by unitsSMulGroup is exactly the second component of the image of g under the complement-related equivalence.

Русский

Во второй компоненте пары из unitsSMulGroup совпадает второй элемент изображения g через соответствующее отображение-комплемента.

LaTeX

$$$\\mathrm{snd}\\big(\\mathrm{unitsSMulGroup}(\\varphi,d,u,g)\\big) = ((d^{\\mathrm{compl}}(u)).\\mathrm{equiv} \\; g).2.$$$

Lean4

theorem unitsSMulGroup_snd (u : ℤˣ) (g : G) : (unitsSMulGroup φ d u g).2 = ((d.compl u).equiv g).2 := by
  rcases Int.units_eq_one_or u with rfl | rfl <;> rfl

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