toNonUnitalSubring_injective — Mathlib

English

The forgetful map from NonUnitalSubalgebra to NonUnitalSubring is injective.

Русский

Отображение от NonUnitalSubalgebra к NonUnitalSubring инъективно.

LaTeX

$$$\text{Injective}(\text{toNonUnitalSubring})$$$

Lean4

theorem toNonUnitalSubring_injective :
    Function.Injective (toNonUnitalSubring : NonUnitalSubalgebra R A → NonUnitalSubring A) := fun S T h =>
  ext fun x => by rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

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