subringCongr — Mathlib

English

If s = t as subrings of a ring R, then there is a canonical ring isomorphism between s and t, given by the identity on the underlying sets.

Русский

Если подкольца s и t равны как подкольца кольца R, существует каноническое кольцевое изоморфизм между s и t, заданное идентичностью на множествах.

LaTeX

$$$ h : s = t \\Rightarrow s \\cong^+_* t $$$

Lean4

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

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