Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-20 23:14 3762d96a

View on Github →

feat(ring_theory/ideals): lift for quotient rings (#529)

Estimated changes

Modified ring_theory/ideals.lean

added theorem ideal.ext

added def ideal.is_coprime

added theorem ideal.is_coprime_def

added theorem ideal.is_coprime_self

added theorem ideal.mem_span_pair

added def ideal.quotient.lift

added theorem ideal.quotient.lift_mk