mathlib3
feat(ring_theory): Fractional ideals
#2062
Merged
Overview
Commits
16
Changes
View On GitHub
Commits
  • Some WIP work on fractional ideals
    Vierkantor committed 6 years ago
  • Fill in the `sorry`
    Vierkantor committed 6 years ago
  • A lot of instances for fractional_ideal
    Vierkantor committed 6 years ago
  • Show that an invertible fractional ideal `I` has inverse `1 : I`
    Vierkantor committed 6 years ago
  • Cleanup and documentation
    Vierkantor committed 6 years ago
  • Move `has_div submodule` to algebra_operations
    Vierkantor committed 6 years ago
  • More cleanup and documentation
    Vierkantor committed 6 years ago
  • Explain the `non_zero_divisors R` in the `quotient` section
    Vierkantor committed 6 years ago
  • whitespace
    Vierkantor committed 6 years ago
  • `has_inv` instance for `fractional_ideal`
    Vierkantor committed 6 years ago
  • `set.univ.image` -> `set.range`
    Vierkantor committed 6 years ago
  • Fix: `mem_div_iff.mpr` should be `mem_div_iff.mp`
    Vierkantor committed 6 years ago
  • Add `mem_div_iff_smul_subset`
    Vierkantor committed 6 years ago
  • whitespace again
    Vierkantor committed 6 years ago
  • Fix unused argument to `inv_nonzero`
    Vierkantor committed 6 years ago
  • Merge branch 'master' into fractional_ideal
    mergify[bot] committed 6 years ago
FAQ Terms Privacy Refunds Impressum
Loading