Theorem Ideal.span_single_eq_top

Modification history

2025-12-20 21:16
Mathlib/RingTheory/Ideal/Basic.lean
feat(RingTheory/FinitePresentation): a finite product of finitely presented algebras is finitely presented (#32758) …
Added Ideal.span_single_eq_topView on Github →