toSubring_injective — Mathlib

English

The map toSubring: ValuationSubring K → Subring K is injective; distinct valuation subrings have distinct carrier subrings.

Русский

Отображение toSubring: ValuationSubring K → Subring K инъективно; различные валюационные подкольца имеют разные носители.

LaTeX

$$$\text{toSubring}: \text{ValuationSubring}(K) \to \text{Subring}(K)$ is injective, i.e., if $A.toSubring = B.toSubring$ then $A = B$.$$

Lean4

theorem toSubring_injective : Function.Injective (toSubring : ValuationSubring K → Subring K) := fun x y h => by
  cases x; cases y; congr

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