toSubalgebra_injective — Mathlib

English

The map that sends a star-subalgebra to its underlying Subalgebra is injective.

Русский

Отображение звездной подалгебры в соответствующую подалгебру по Carrier инъективно.

LaTeX

$$$\text{toSubalgebra} : \text{StarSubalgebra} \; R \; A \to \text{Subalgebra} \; R \; A$ is injective.$$

Lean4

theorem toSubalgebra_injective : Function.Injective (toSubalgebra : StarSubalgebra R A → Subalgebra R A) := fun S T h =>
  ext fun x => by rw [← mem_toSubalgebra, ← mem_toSubalgebra, h]

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