Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_field.is_principal_ideal_ring

Modification history

2021-10-19 09:31
src/ring_theory/principal_ideal_domain.lean
refactor(algebra/domain): make domain and integral_domain mixins (#9719) …
Modified is_field.is_principal_ideal_ringView on Github →
2021-07-27 19:34
src/ring_theory/principal_ideal_domain.lean
feat(ring_theory): `is_dedekind_domain_inv` implies `is_dedekind_domain` (#8315) …
Added is_field.is_principal_ideal_ringView on Github →