Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-16 10:12 22eba86c

View on Github →

feat(*): add some missing coe_* lemmas (#6697)

  • add submonoid.coe_pow, submonoid.coe_list_prod, submonoid.coe_multiset_prod, submonoid.coe_finset_prod, subring.coe_pow, subring.coe_nat_cast, subring.coe_int_cast;
  • add rat.num_div_denom;
  • add inv_of_pow.

Estimated changes

added theorem inv_of_pow
added theorem rat.num_div_denom
added theorem submonoid.coe_pow
modified theorem submonoid.pow_mem
added theorem subring.coe_int_cast
added theorem subring.coe_nat_cast
added theorem subring.coe_pow