Skip to content

refactor(RingTheory/Ideal/Heoght): minimize usages of Ideal.primeHeight#37500

Open
Thmoas-Guan wants to merge 30 commits intoleanprover-community:masterfrom
Thmoas-Guan:minimalPrimes-API
Open

refactor(RingTheory/Ideal/Heoght): minimize usages of Ideal.primeHeight#37500
Thmoas-Guan wants to merge 30 commits intoleanprover-community:masterfrom
Thmoas-Guan:minimalPrimes-API

Commits

Commits on Apr 1, 2026

Commits on Apr 2, 2026

Commits on Apr 3, 2026

Commits on Apr 4, 2026

Commits on Apr 6, 2026

Commits on Apr 13, 2026

Commits on Apr 14, 2026