Commit 2024-04-18 10:42 a445a6b0
View on Github →fix: strengthen Dirichlet Unit Theorem (#12240)
The theorem NumberField.Units.exist_unique_eq_mul_prod was using nested ∃!'s rather than a single ∃!.
fix: strengthen Dirichlet Unit Theorem (#12240)
The theorem NumberField.Units.exist_unique_eq_mul_prod was using nested ∃!'s rather than a single ∃!.