Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-17 17:16 980a01e8

View on Github →

feat(ring_theory/ideals): quotient rings (#196)

Estimated changes

Modified ring_theory/ideals.lean

added theorem is_ideal.exists_inv

added theorem is_ideal.mul_left

added theorem is_ideal.mul_right

added theorem is_ideal.neg_iff

added def is_ideal.quotient

added theorem is_ideal.quotient_eq_zero_iff_mem

added def is_ideal.quotient_rel

added theorem is_proper_ideal_iff_one_not_mem

deleted theorem not_unit_of_mem_maximal_ideal

added theorem not_unit_of_mem_proper_ideal