nonUnitalSubringCongr — Mathlib

English

Let s ⊆ R with closure(s) = ⊤. If f,g: R →ₙ+* S satisfy EqOn f g on s, then f = g.

Русский

Пусть s ⊆ R так, что closure(s)=⊤. Если f,g: R →ₙ+* S удовлетворяют EqOn на s, тогда f=g.

LaTeX

$$$\overline{s}=\top \Rightarrow (s.EqOn f g) \Rightarrow f=g$$$

Lean4

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

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