Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ideal.is_prime.is_primary

Modification history

2022-03-08 08:31
src/ring_theory/ideal/operations.lean
fix(ring_theory/ideal/operations): fix a name and dot notation (#12507)
Added ideal.is_prime.is_primaryView on Github →