Theorem one_mem_inv_coe_ideal

Modification history

2026-04-17 15:37

Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean

chore(RingTheory/DedekindDomain/Ideal/*): move decls into namespaces (#38133) …

Deleted one_mem_inv_coe_ideal View on Github →

2025-07-31 15:44

Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean

chore: split long file `DedekindDomain/Ideal.lean` (#27676) …

Modified one_mem_inv_coe_ideal View on Github →

2024-03-27 11:32

Mathlib/RingTheory/DedekindDomain/Ideal.lean

feat(DedekindDomain.Ideal): remove Domain assumption from DedekindDomain (#11527) …

Added one_mem_inv_coe_ideal View on Github →