Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-12 13:39 3f216bc6

View on Github →

feat(number_theory/basic): dvd_sub_pow_of_dvd_sub (#2640) Co-authored with: Kenny Lau kc_kennylau@yahoo.com.hk

Estimated changes

Modified src/algebra/geom_sum.lean

added theorem geom_series₂_self

added theorem ring_hom.map_geom_series

added theorem ring_hom.map_geom_series₂

Created src/number_theory/basic.lean

added theorem dvd_sub_pow_of_dvd_sub

Modified src/ring_theory/ideals.lean

added theorem ideal.quotient.mk_eq_mk_hom