Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-10 08:50 54ce15b5

View on Github →

refactor(ring_theory/ideals): avoid using type class inference for setoids in quotient rings and groups (#212)

Estimated changes

added theorem is_group_hom.gpow
added theorem is_group_hom.pow
added theorem quotient.exact'
added theorem quotient.mk_out'
added theorem quotient.out_eq'
added theorem quotient.sound'
added theorem left_cosets.coe_gpow
added theorem left_cosets.coe_inv
added theorem left_cosets.coe_mul
added theorem left_cosets.coe_one
added theorem left_cosets.coe_pow
added def left_cosets.mk
deleted theorem is_ideal.exists_inv
deleted def is_ideal.quotient
added def is_ideal.trivial
added theorem quotient_ring.coe_add
added theorem quotient_ring.coe_mul
added theorem quotient_ring.coe_neg
added theorem quotient_ring.coe_one
added theorem quotient_ring.coe_pow
added theorem quotient_ring.coe_sub
added theorem quotient_ring.coe_zero
added def quotient_ring.mk