toSubsemiring_injective — Mathlib

English

The map sending a subalgebra to its underlying subsemiring is injective.

Русский

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

LaTeX

$$$ S \\mapsto S^{\\mathrm{toSubsemiring}} \quad \\text{is injective}$$$

Lean4

theorem toSubsemiring_injective : Function.Injective (toSubsemiring : Subalgebra R A → Subsemiring A) := fun S T h =>
  ext fun x => by rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

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