Skip to content

[Merged by Bors] - refactor(RingTheory/Ideal/Height): make Ideal.primeHeight private#37627

Closed
Thmoas-Guan wants to merge 119 commits into
leanprover-community:masterfrom
Thmoas-Guan:refactor-primeHeight
Closed

[Merged by Bors] - refactor(RingTheory/Ideal/Height): make Ideal.primeHeight private#37627
Thmoas-Guan wants to merge 119 commits into
leanprover-community:masterfrom
Thmoas-Guan:refactor-primeHeight

Commits

Commits on Apr 1, 2026

Commits on Apr 2, 2026

Commits on Apr 3, 2026

Commits on Apr 4, 2026

Commits on May 5, 2026

Commits on May 7, 2026

Commits on May 8, 2026

Commits on May 12, 2026

Commits on May 13, 2026

Commits on May 17, 2026

Commits on May 18, 2026

Commits on May 21, 2026