Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 15:19 113ab32f

View on Github →

feat(ring_theory/power_series/basic): API about inv (#11617) Also rename protected lemmas mul_inv to mul_inv_cancel inv_mul to inv_mul_cancel

Estimated changes

Modified src/number_theory/bernoulli.lean

Modified src/ring_theory/power_series/basic.lean

added theorem mv_power_series.C_inv

added theorem mv_power_series.X_inv

added theorem mv_power_series.one_inv

added theorem mv_power_series.smul_eq_C_mul

added theorem mv_power_series.smul_inv

added theorem mv_power_series.zero_inv

added theorem polynomial.constant_coeff_coe

added theorem power_series.C_inv

added theorem power_series.X_inv

added theorem power_series.one_inv

added theorem power_series.smul_eq_C_mul

added theorem power_series.smul_inv

added theorem power_series.zero_inv