Commit 2024-01-31 10:21 9d1a7d26

View on Github →

feat: The support of f ^ n (#9617) This involves moving lemmas from Algebra.GroupPower.Ring to Algebra.GroupWithZero.Basic and changing some 0 < n assumptions to n ≠ 0. From LeanAPAP

Estimated changes

added theorem Function.support_div'
modified theorem Function.support_div
added theorem Function.support_inv'
modified theorem Function.support_inv
added theorem Function.support_mul'
modified theorem Function.support_mul
added theorem Function.support_pow'
added theorem Function.support_pow
modified theorem pow_pos_iff
deleted theorem ne_zero_pow
deleted theorem pow_eq_zero
deleted theorem pow_eq_zero_iff'
deleted theorem pow_eq_zero_iff
deleted theorem pow_eq_zero_of_le
deleted theorem pow_ne_zero
deleted theorem pow_ne_zero_iff
deleted theorem sq_eq_zero_iff
deleted theorem zero_pow'
deleted theorem zero_pow
deleted theorem zero_pow_eq
deleted theorem zero_pow_eq_zero
added theorem ne_zero_pow
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_zero_iff
added theorem zero_pow
added theorem zero_pow_eq
added theorem zero_pow_eq_zero
modified theorem Even.pow_pos_iff
modified theorem MulChar.pow_apply'