gc — Mathlib · SciLib

English

There is a Galois connection between toIdeal and Ideal.homogeneousCore 𝒜.

Русский

Существует связь Гало между toIdeal и Ideal.homogeneousCore 𝒜.

LaTeX

$$$ \text{GaloisConnection}(\text{toIdeal}, \text{Ideal.homogeneousCore } 𝒜) $$$

Lean4

theorem gc : GaloisConnection toIdeal (Ideal.homogeneousCore 𝒜) := fun I _ =>
  ⟨fun H => I.toIdeal_homogeneousCore_eq_self ▸ Ideal.homogeneousCore_mono 𝒜 H, fun H =>
    le_trans H (Ideal.homogeneousCore'_le _ _)⟩

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