Commit 2022-12-13 21:37 90cb7f70

View on Github →

feat: port Algebra.GroupPower.Ring (#979) Mathlib SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GroupPower/Ring.lean

added theorem Ring.inverse_pow

added theorem add_sq'

added theorem add_sq

added theorem coe_powMonoidWithZeroHom

added theorem eq_or_eq_neg_of_sq_eq_sq

added theorem min_pow_dvd_add

added theorem mul_neg_one_pow_eq_zero_iff

added theorem ne_zero_pow

added theorem neg_one_pow_eq_or

added theorem neg_one_pow_mul_eq_zero_iff

added theorem neg_one_sq

added theorem neg_pow

added theorem neg_pow_bit0

added theorem neg_pow_bit1

added theorem neg_sq

added def powMonoidWithZeroHom

added theorem powMonoidWithZeroHom_apply

added theorem pow_dvd_pow_iff

added theorem pow_eq_zero

added theorem pow_eq_zero_iff'

added theorem pow_eq_zero_iff

added theorem pow_eq_zero_of_le

added theorem pow_ne_zero

added theorem pow_ne_zero_iff

added theorem sq_eq_one_iff

added theorem sq_eq_sq_iff_eq_or_eq_neg

added theorem sq_eq_zero_iff

added theorem sq_ne_one_iff

added theorem sq_sub_sq

added theorem sub_sq'

added theorem sub_sq

added theorem zero_pow'

added theorem zero_pow

added theorem zero_pow_eq

added theorem zero_pow_eq_zero

Modified Mathlib/Tactic/Positivity/Basic.lean

deleted theorem pow_ne_zero