refl — Mathlib

English

The N-conjugacy relation on splittings is reflexive: every splitting is N-conjugate to itself, realized by the identity in N.

Русский

Отношение N-конъюгированности на разложениях рефлексивно: каждое разложение конъюгировано к самому себе, реализуется через тождественный элемент в N.

LaTeX

$$$\\forall s \\in S.Splitting,\\ S.IsConj(s,s)$$$

Lean4

/-- `N`-conjugacy is reflexive. -/
@[to_additive /-- `N`-conjugacy is reflexive. -/
    ]
theorem refl (s : S.Splitting) : S.IsConj s s :=
  ⟨1, by simp only [map_one, inv_one, one_mul, mul_one]⟩

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