Skip to content

Commit

Permalink
chore(ring_theory): set_like instance for fractional ideals (#8275)
Browse files Browse the repository at this point in the history
This PR does a bit of cleanup in `fractional_ideal.lean` by using `set_like` to define `has_mem` and the coe to set.

As a bonus, it removes the `namespace ring` at the top of the file, that has been bugging me ever after I added it in the original fractional ideal PR.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
  • Loading branch information
Vierkantor and Vierkantor committed Jul 22, 2021
1 parent 38ac9ba commit 7cdd702
Show file tree
Hide file tree
Showing 3 changed files with 102 additions and 93 deletions.
2 changes: 1 addition & 1 deletion docs/overview.yaml
Expand Up @@ -58,7 +58,7 @@ General algebra:
maximal ideal: 'ideal.is_maximal'
Chinese remainder theorem: 'ideal.quotient_inf_ring_equiv_pi_quotient'
localization: 'localization'
fractional ideal: 'ring.fractional_ideal'
fractional ideal: 'fractional_ideal'
first isomorphism theorem for commutative rings: 'ring_hom.quotient_ker_equiv_of_surjective'

Divisibility in integral domains:
Expand Down
2 changes: 1 addition & 1 deletion src/ring_theory/dedekind_domain.lean
Expand Up @@ -229,7 +229,7 @@ TODO: prove the equivalence.
def is_dedekind_domain_inv : Prop :=
∀ I ≠ (⊥ : fractional_ideal A⁰ (fraction_ring A)), I * (1 / I) = 1

open ring.fractional_ideal
open fractional_ideal

lemma is_dedekind_domain_inv_iff (K : Type*) [field K] [algebra A K] [is_fraction_ring A K] :
is_dedekind_domain_inv A ↔
Expand Down

0 comments on commit 7cdd702

Please sign in to comment.