ext_ring — Mathlib

English

If two σ-linear maps agree on 1, they are equal as maps (extensionality principle for σ-linear maps).

Русский

Если два σ-линейных отображения совпадают на единице, они равны как отображения (принцип экстенсивности).

LaTeX

$$$ f 1 = g 1 \Rightarrow f = g $$$

Lean4

/-- If two `σ`-linear maps from `R` are equal on `1`, then they are equal. -/
@[ext high]
theorem ext_ring {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g :=
  ext fun x ↦ by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]

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