Commit 2025-11-21 08:42 f9aa5367
View on Github →feat: inf of principal ideals is principal ideal of lcm (#31867)
A basic lemma that seems to be missing from mathlib: I used this when teaching ring theory in the Lean course with fpvandoorn.
feat: inf of principal ideals is principal ideal of lcm (#31867)
A basic lemma that seems to be missing from mathlib: I used this when teaching ring theory in the Lean course with fpvandoorn.