subfieldCongr — Mathlib

English

If two subfields s and t of a division ring K are equal, then the natural identity map induces a ring isomorphism between them.

Русский

Если два подполя s и t над K совпадают, то естественное тождественное отображение порождает кольцевое изоморфизм между ними.

LaTeX

$$$ s=t \\Rightarrow s \\cong+* t $$$

Lean4

/-- Makes the identity isomorphism from a proof two subfields of a multiplicative
    monoid are equal. -/
def subfieldCongr (h : s = t) : s ≃+* t :=
  { Equiv.setCongr <| SetLike.ext'_iff.1 h with
    map_mul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl }

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