feat(ring_theory): Fractional ideals #2062
mergify
merged
16 commits into
leanprover-community:master
from
Vierkantor:fractional_ideal
Some WIP work on fractional ideals
dfa37f62
Fill in the `sorry`
5397a149
A lot of instances for fractional_ideal
ae168b5a
Show that an invertible fractional ideal `I` has inverse `1 : I`
ed96262e
Cleanup and documentation
3ab5e71c
Move `has_div submodule` to algebra_operations
855696bf
More cleanup and documentation
e3af5426
Explain the `non_zero_divisors R` in the `quotient` section
0cbfe0fa
kim-em
commented
on 2020-02-26
whitespace
c0b1f53b
`has_inv` instance for `fractional_ideal`
71112b76
`set.univ.image` -> `set.range`
fb9bab4d
Fix: `mem_div_iff.mpr` should be `mem_div_iff.mp`
26a70474
Add `mem_div_iff_smul_subset`
e9ff816a
whitespace again
42455756
Fix unused argument to `inv_nonzero`
5b1fdb9e
jcommelin
approved these changes
on 2020-02-28
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into fractional_ideal
46c6f854
Login to write a write a comment.
Login via GitHub