irreducible_pow_sup — Mathlib

English

Re-statement of irreducible_pow_sup: J^n ⊔ I = J^n for irreducible J and suitable n.

Русский

Повторение irreducible_pow_sup: J^n ⊔ I = J^n для неразложимого J и подходящего n.

LaTeX

$$J^n ⊔ I = J^n$$

Lean4

theorem irreducible_pow_sup [DecidableEq (Ideal T)] (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) :
    J ^ n ⊔ I = J ^ min ((normalizedFactors I).count J) n := by
  rw [sup_eq_prod_inf_factors (pow_ne_zero n hJ.ne_zero) hI, min_comm, normalizedFactors_of_irreducible_pow hJ,
    normalize_eq J, replicate_inter, prod_replicate]

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