Theorems · Theorem · commutative algebra

Ideal.coe_piOrderIso_apply

∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] [inst_1 : Finite ι] (a : Ideal ((i : ι) → R i))
  (i : ι), ↑(Ideal.piOrderIso a i) = ⋂ s, ⋂ (_ : ↑a ⊆ (fun a => a i) ⁻¹' ↑s), ↑s

Defined in

Mathlib.RingTheory.Ideal.Maps

Cited by

0 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringFinite