le_def — Mathlib

English

`A` dominates `B` iff `B ≤ A` as subrings and `m_A ∩ B = m_B`.

Русский

Покрытие A превосходит B, если B ⊆ A как подкольца и пересечение максимальных идеалов совпадает: m_A ∩ B = m_B.

LaTeX

$$A ≤ B ↔ ∃ h : A.toSubring ≤ B.toSubring, IsLocalHom (Subring.inclusion h)$$

Lean4

/-- `A` dominates `B` if and only if `B ≤ A` (as subrings) and `m_A ∩ B = m_B`. -/
theorem le_def {A B : LocalSubring R} : A ≤ B ↔ ∃ h : A.toSubring ≤ B.toSubring, IsLocalHom (Subring.inclusion h) :=
  Iff.rfl

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