Commit 2025-07-24 08:42 29caf88d

View on Github →

chore: split Data.Sign (#27232) We now have a Defs file defining SignType and basic instances, as well as a Basic file proving results about the sign function on a ring. The files have not been changed beyond updating the module description.

Estimated changes

deleted theorem Int.sign_eq_sign
deleted theorem Left.sign_neg
deleted theorem Right.sign_neg
deleted def SignType.cast
deleted def SignType.castHom
deleted theorem SignType.coe_mul
deleted theorem SignType.coe_neg
deleted theorem SignType.coe_neg_one
deleted theorem SignType.coe_one
deleted theorem SignType.coe_pow
deleted theorem SignType.coe_zero
deleted theorem SignType.coe_zpow
deleted def SignType.fin3Equiv
deleted theorem SignType.intCast_cast
deleted theorem SignType.le_neg_one_iff
deleted theorem SignType.le_one
deleted theorem SignType.lt_one_iff
deleted theorem SignType.map_cast'
deleted theorem SignType.map_cast
deleted theorem SignType.neg_eq_neg_one
deleted theorem SignType.neg_eq_self_iff
deleted theorem SignType.neg_iff
deleted theorem SignType.neg_one_le
deleted theorem SignType.neg_one_lt_iff
deleted theorem SignType.neg_one_lt_one
deleted theorem SignType.nonneg_iff
deleted theorem SignType.nonpos_iff
deleted theorem SignType.not_lt_neg_one
deleted theorem SignType.not_one_lt
deleted theorem SignType.one_le_iff
deleted theorem SignType.pos_eq_one
deleted theorem SignType.pos_iff
deleted theorem SignType.pow_even
deleted theorem SignType.pow_odd
deleted theorem SignType.range_eq
deleted theorem SignType.self_eq_neg_iff
deleted def SignType.sign
deleted theorem SignType.univ_eq
deleted theorem SignType.zero_eq_zero
deleted theorem SignType.zpow_even
deleted theorem SignType.zpow_odd
deleted inductive SignType
deleted theorem StrictMono.sign_comp
deleted theorem abs_mul_sign
deleted theorem exists_signed_sum'
deleted theorem exists_signed_sum
deleted theorem self_mul_sign
deleted def signHom
deleted theorem sign_apply
deleted theorem sign_eq_neg_one_iff
deleted theorem sign_eq_one_iff
deleted theorem sign_eq_zero_iff
deleted theorem sign_intCast
deleted theorem sign_mul
deleted theorem sign_mul_abs
deleted theorem sign_mul_self
deleted theorem sign_ne_zero
deleted theorem sign_neg
deleted theorem sign_nonneg_iff
deleted theorem sign_nonpos_iff
deleted theorem sign_one
deleted theorem sign_pos
deleted theorem sign_pow
deleted theorem sign_sum
deleted theorem sign_zero
added def SignType.castHom
added theorem SignType.coe_mul
added theorem SignType.coe_pow
added theorem SignType.coe_zpow
added theorem SignType.intCast_cast
added theorem SignType.pow_even
added theorem SignType.pow_odd
added theorem SignType.range_eq
added theorem SignType.univ_eq
added theorem SignType.zpow_even
added theorem SignType.zpow_odd
added theorem abs_mul_sign
added theorem exists_signed_sum'
added theorem exists_signed_sum
added theorem self_mul_sign
added def signHom
added theorem sign_intCast
added theorem sign_mul
added theorem sign_mul_abs
added theorem sign_mul_self
added theorem sign_pow
added theorem sign_sum
added theorem Int.sign_eq_sign
added theorem Left.sign_neg
added theorem Right.sign_neg
added def SignType.cast
added theorem SignType.coe_neg
added theorem SignType.coe_neg_one
added theorem SignType.coe_one
added theorem SignType.coe_zero
added theorem SignType.le_one
added theorem SignType.lt_one_iff
added theorem SignType.map_cast'
added theorem SignType.map_cast
added theorem SignType.neg_iff
added theorem SignType.neg_one_le
added theorem SignType.nonneg_iff
added theorem SignType.nonpos_iff
added theorem SignType.not_one_lt
added theorem SignType.one_le_iff
added theorem SignType.pos_eq_one
added theorem SignType.pos_iff
added def SignType.sign
added theorem SignType.zero_eq_zero
added inductive SignType
added theorem StrictMono.sign_comp
added theorem sign_apply
added theorem sign_eq_neg_one_iff
added theorem sign_eq_one_iff
added theorem sign_eq_zero_iff
added theorem sign_ne_zero
added theorem sign_neg
added theorem sign_nonneg_iff
added theorem sign_nonpos_iff
added theorem sign_one
added theorem sign_pos
added theorem sign_zero