mathlib

a6b1f1c6 - `lemma ideal.homogenisation.eq_Sup [Π (i : ι) (x : A i), decidable (x ≠ 0)] `