Commit 2025-04-13 02:25 72561137

View on Github →

chore(*): rename ring type variables (#23939) ... in some files. Also change some NeZero (α := _) 1 to NeZero (1 : _).

Estimated changes

modified theorem Commute.mul_geom_sum₂
modified theorem Commute.mul_neg_geom_sum₂
modified theorem Commute.sub_dvd_pow_sub_pow
modified theorem Odd.add_dvd_pow_add_pow
modified theorem Odd.geom_sum_pos
modified theorem RingHom.map_geom_sum
modified theorem RingHom.map_geom_sum₂
modified theorem geom_sum_Ico'
modified theorem geom_sum_Ico
modified theorem geom_sum_Ico_le_of_lt_one
modified theorem geom_sum_Ico_mul
modified theorem geom_sum_Ico_mul_neg
modified theorem geom_sum_eq
modified theorem geom_sum_inv
modified theorem geom_sum_lt
modified theorem geom_sum_mul
modified theorem geom_sum_mul_add
modified theorem geom_sum_mul_neg
modified theorem geom_sum_mul_of_le_one
modified theorem geom_sum_mul_of_one_le
modified theorem geom_sum_ne_zero
modified theorem geom_sum_neg_iff
modified theorem geom_sum_of_lt_one
modified theorem geom_sum_of_one_lt
modified theorem geom_sum_one
modified theorem geom_sum_pos'
modified theorem geom_sum_pos
modified theorem geom_sum_pos_and_lt_one
modified theorem geom_sum_pos_iff
modified theorem geom_sum_succ'
modified theorem geom_sum_succ
modified theorem geom_sum_two
modified theorem geom_sum_zero
modified theorem geom_sum₂_Ico
modified theorem geom_sum₂_comm
modified theorem geom_sum₂_mul
modified theorem geom_sum₂_mul_add
modified theorem geom_sum₂_mul_of_ge
modified theorem geom_sum₂_mul_of_le
modified theorem geom_sum₂_self
modified theorem geom_sum₂_succ_eq
modified theorem geom_sum₂_with_one
modified theorem geom₂_sum
modified theorem geom₂_sum_of_gt
modified theorem geom₂_sum_of_lt
modified theorem mul_geom_sum
modified theorem mul_geom_sum₂_Ico
modified theorem mul_neg_geom_sum
modified theorem neg_one_geom_sum
modified theorem one_geom_sum
modified theorem one_sub_dvd_one_sub_pow
modified theorem op_geom_sum
modified theorem op_geom_sum₂
modified theorem sub_dvd_pow_sub_pow
modified theorem sub_one_dvd_pow_sub_one
modified theorem zero_geom_sum
modified structure LinearOrderedField
modified structure LinearOrderedSemifield
modified theorem inv_mul_le_one
modified theorem mul_inv_le_one
modified theorem Int.add_one_le_ceil_iff
modified theorem Int.ceil_add_ceil_le
modified theorem Int.ceil_add_intCast
modified theorem Int.ceil_add_le
modified theorem Int.ceil_add_natCast
modified theorem Int.ceil_add_ofNat
modified theorem Int.ceil_add_one
modified theorem Int.ceil_eq_on_Ioc'
modified theorem Int.ceil_eq_on_Ioc
modified theorem Int.ceil_eq_self_iff_mem
modified theorem Int.ceil_eq_zero_iff
modified theorem Int.ceil_intCast
modified theorem Int.ceil_le_floor_add_one
modified theorem Int.ceil_lt_add_one
modified theorem Int.ceil_mono
modified theorem Int.ceil_natCast
modified theorem Int.ceil_ofNat
modified theorem Int.ceil_one
modified theorem Int.ceil_sub_intCast
modified theorem Int.ceil_sub_natCast
modified theorem Int.ceil_sub_ofNat
modified theorem Int.ceil_sub_one
modified theorem Int.ceil_sub_self_eq
modified theorem Int.ceil_zero
modified theorem Int.floor_add_fract
modified theorem Int.floor_add_intCast
modified theorem Int.floor_add_natCast
modified theorem Int.floor_add_ofNat
modified theorem Int.floor_add_one
modified theorem Int.floor_congr
modified theorem Int.floor_eq_on_Ico'
modified theorem Int.floor_eq_on_Ico
modified theorem Int.floor_eq_self_iff_mem
modified theorem Int.floor_eq_zero_iff
modified theorem Int.floor_fract
modified theorem Int.floor_intCast
modified theorem Int.floor_intCast_add
modified theorem Int.floor_le_ceil
modified theorem Int.floor_lt_ceil_of_lt
modified theorem Int.floor_mono
modified theorem Int.floor_natCast
modified theorem Int.floor_natCast_add
modified theorem Int.floor_ofNat
modified theorem Int.floor_ofNat_add
modified theorem Int.floor_one
modified theorem Int.floor_sub_intCast
modified theorem Int.floor_sub_natCast
modified theorem Int.floor_sub_ofNat
modified theorem Int.floor_sub_one
modified theorem Int.floor_zero
modified theorem Int.fract_add
modified theorem Int.fract_add_floor
modified theorem Int.fract_add_fract_le
modified theorem Int.fract_add_intCast
modified theorem Int.fract_add_le
modified theorem Int.fract_add_natCast
modified theorem Int.fract_add_ofNat
modified theorem Int.fract_add_one
modified theorem Int.fract_eq_fract
modified theorem Int.fract_eq_iff
modified theorem Int.fract_eq_self
modified theorem Int.fract_floor
modified theorem Int.fract_fract
modified theorem Int.fract_intCast
modified theorem Int.fract_intCast_add
modified theorem Int.fract_lt_one
modified theorem Int.fract_mul_natCast
modified theorem Int.fract_natCast
modified theorem Int.fract_natCast_add
modified theorem Int.fract_neg
modified theorem Int.fract_neg_eq_zero
modified theorem Int.fract_nonneg
modified theorem Int.fract_ofNat_add
modified theorem Int.fract_one
modified theorem Int.fract_one_add
modified theorem Int.fract_sub_intCast
modified theorem Int.fract_sub_natCast
modified theorem Int.fract_sub_ofNat
modified theorem Int.fract_sub_one
modified theorem Int.fract_sub_self
modified theorem Int.fract_zero
modified theorem Int.image_fract
modified theorem Int.le_floor_add
modified theorem Int.le_floor_add_floor
modified theorem Int.lt_floor_add_one
modified theorem Int.lt_succ_floor
modified theorem Int.map_ceil
modified theorem Int.map_floor
modified theorem Int.map_fract
modified theorem Int.preimage_Icc
modified theorem Int.preimage_Ici
modified theorem Int.preimage_Ico
modified theorem Int.preimage_Iic
modified theorem Int.preimage_Iio
modified theorem Int.preimage_Ioc
modified theorem Int.preimage_Ioi
modified theorem Int.preimage_Ioo
modified theorem Int.preimage_ceil_singleton
modified theorem Int.preimage_fract
modified theorem Int.self_sub_floor
modified theorem Int.self_sub_fract
modified theorem Int.sub_one_lt_floor
modified theorem subsingleton_floorRing
modified theorem Nat.add_one_le_ceil_iff
modified theorem Nat.ceil_add_le
modified theorem Nat.ceil_intCast
modified theorem Nat.ceil_le_floor_add_one
modified theorem Nat.ceil_lt_add_one
modified theorem Nat.ceil_mono
modified theorem Nat.ceil_natCast
modified theorem Nat.ceil_ofNat
modified theorem Nat.ceil_one
modified theorem Nat.ceil_zero
modified theorem Nat.floor_add_natCast
modified theorem Nat.floor_congr
modified theorem Nat.floor_div_eq_div
modified theorem Nat.floor_div_natCast
modified theorem Nat.floor_div_ofNat
modified theorem Nat.floor_eq_on_Ico
modified theorem Nat.floor_le
modified theorem Nat.floor_le_ceil
modified theorem Nat.floor_mono
modified theorem Nat.floor_natCast
modified theorem Nat.floor_ofNat
modified theorem Nat.floor_one
modified theorem Nat.floor_sub_natCast
modified theorem Nat.floor_sub_ofNat
modified theorem Nat.floor_sub_one
modified theorem Nat.floor_zero
modified theorem Nat.le_ceil
modified theorem Nat.le_floor_iff'
modified theorem Nat.lt_floor_add_one
modified theorem Nat.lt_succ_floor
modified theorem Nat.map_ceil
modified theorem Nat.map_floor
modified theorem Nat.one_le_floor_iff
modified theorem Nat.preimage_Icc
modified theorem Nat.preimage_Ici
modified theorem Nat.preimage_Ico
modified theorem Nat.preimage_Iic
modified theorem Nat.preimage_Iio
modified theorem Nat.preimage_Ioc
modified theorem Nat.preimage_Ioi
modified theorem Nat.preimage_Ioo
modified theorem Nat.preimage_ceil_zero
modified theorem Nat.preimage_floor_zero
modified theorem Nat.sub_one_lt_floor
modified theorem subsingleton_floorSemiring
modified theorem Set.Icc.coe_eq_one
modified theorem Set.Icc.coe_eq_zero
modified theorem Set.Icc.coe_le_one
modified theorem Set.Icc.coe_mul
modified theorem Set.Icc.coe_ne_one
modified theorem Set.Icc.coe_ne_zero
modified theorem Set.Icc.coe_nonneg
modified theorem Set.Icc.coe_one
modified theorem Set.Icc.coe_pow
modified theorem Set.Icc.coe_zero
modified theorem Set.Icc.le_one
modified theorem Set.Icc.mk_one
modified theorem Set.Icc.mk_zero
modified theorem Set.Icc.mul_le_left
modified theorem Set.Icc.mul_le_right
modified theorem Set.Icc.nonneg
modified theorem Set.Ico.coe_eq_zero
modified theorem Set.Ico.coe_lt_one
modified theorem Set.Ico.coe_mul
modified theorem Set.Ico.coe_ne_zero
modified theorem Set.Ico.coe_nonneg
modified theorem Set.Ico.coe_zero
modified theorem Set.Ico.mk_zero
modified theorem Set.Ico.nonneg
modified theorem Set.Ioc.coe_eq_one
modified theorem Set.Ioc.coe_le_one
modified theorem Set.Ioc.coe_mul
modified theorem Set.Ioc.coe_ne_one
modified theorem Set.Ioc.coe_one
modified theorem Set.Ioc.coe_pos
modified theorem Set.Ioc.coe_pow
modified theorem Set.Ioc.le_one
modified theorem Set.Ioc.mk_one
modified theorem Set.Ioo.coe_mul
modified theorem Set.Ioo.lt_one
modified theorem Set.Ioo.pos
modified structure CanonicallyOrderedCommSemiring
modified theorem Odd.pos
modified theorem mul_self_tsub_mul_self
modified theorem mul_self_tsub_one
modified theorem mul_tsub
modified theorem mul_tsub_one
modified theorem sq_tsub_sq
modified theorem tsub_mul
modified theorem tsub_one_mul
modified theorem IsOrderedRing.of_mul_nonneg
modified structure LinearOrderedCommRing
modified structure LinearOrderedCommSemiring
modified structure LinearOrderedRing
modified structure LinearOrderedSemiring
modified structure OrderedCommRing
modified structure OrderedCommSemiring
modified structure OrderedRing
modified structure OrderedSemiring
modified structure StrictOrderedCommRing
modified structure StrictOrderedCommSemiring
modified structure StrictOrderedRing
modified structure StrictOrderedSemiring
modified theorem eq_of_mul_eq_add_eq_one
modified theorem Antitone.mul
modified theorem Antitone.mul_monotone
modified theorem Monotone.mul_antitone
modified theorem StrictAnti.const_mul_of_neg
modified theorem StrictAnti.mul_const_of_neg
modified theorem StrictMono.const_mul_of_neg
modified theorem StrictMono.mul_const_of_neg
modified theorem add_le_mul'
modified theorem add_le_mul
modified theorem add_le_mul_of_left_le_right
modified theorem add_le_mul_of_right_le_left
modified theorem add_le_mul_two_add
modified theorem add_one_le_two_mul
modified theorem antitone_mul_left
modified theorem antitone_mul_right
modified theorem cmp_mul_neg_left
modified theorem cmp_mul_neg_right
modified theorem cmp_mul_pos_left
modified theorem cmp_mul_pos_right
modified theorem four_mul_le_sq_add
modified theorem le_mul_of_le_one_left
modified theorem le_mul_of_le_one_right
modified theorem lt_mul_of_lt_one_left
modified theorem lt_mul_of_lt_one_right
modified theorem lt_two_mul_self
modified theorem max_mul_mul_le_max_mul_max
modified theorem max_mul_of_nonneg
modified theorem min_mul_of_nonneg
modified theorem mul_add_mul_le_mul_add_mul'
modified theorem mul_add_mul_le_mul_add_mul
modified theorem mul_add_mul_lt_mul_add_mul'
modified theorem mul_add_mul_lt_mul_add_mul
modified theorem mul_le_mul_left_of_neg
modified theorem mul_le_mul_of_nonpos_left
modified theorem mul_le_mul_of_nonpos_right
modified theorem mul_le_mul_right_of_neg
modified theorem mul_le_of_one_le_left
modified theorem mul_le_of_one_le_right
modified theorem mul_lt_mul_left_of_neg
modified theorem mul_lt_mul_of_neg_left
modified theorem mul_lt_mul_of_neg_right
modified theorem mul_lt_mul_right_of_neg
modified theorem mul_lt_of_one_lt_left
modified theorem mul_lt_of_one_lt_right
modified theorem mul_max_of_nonneg
modified theorem mul_min_of_nonneg
modified theorem mul_neg_iff
modified theorem mul_nonneg_iff
modified theorem mul_nonneg_iff_of_pos_left
modified theorem mul_nonneg_iff_of_pos_right
modified theorem mul_nonneg_of_three
modified theorem mul_nonpos_iff
modified theorem mul_pos_iff
modified theorem mul_pos_of_neg_of_neg
modified theorem mul_self_inj
modified theorem mul_self_le_mul_self_iff
modified theorem mul_self_lt_mul_self_iff
modified theorem mul_self_nonneg
modified theorem mul_self_pos
modified theorem neg_iff_pos_of_mul_neg
modified theorem nonneg_of_mul_nonneg_left
modified theorem nonneg_of_mul_nonneg_right
modified theorem nonneg_of_mul_nonpos_left
modified theorem nonneg_of_mul_nonpos_right
modified theorem nonpos_of_mul_nonneg_left
modified theorem nonpos_of_mul_nonneg_right
modified theorem nonpos_of_mul_nonpos_left
modified theorem nonpos_of_mul_nonpos_right
modified theorem pos_iff_neg_of_mul_neg
modified theorem pos_of_mul_neg_left
modified theorem pos_of_mul_neg_right
modified theorem sq_nonneg
modified theorem sq_nonpos_iff
modified theorem strictAnti_mul_left
modified theorem strictAnti_mul_right
modified theorem sub_one_lt
modified theorem two_mul_le_add_of_sq_eq_mul
modified theorem two_mul_le_add_sq
modified theorem Ring.inverse_add_inverse
modified theorem Ring.inverse_sub_inverse
modified theorem invOf_add_invOf
modified theorem invOf_neg
modified theorem invOf_sub_invOf
modified theorem invOf_two_add_invOf_two
modified def invertibleNeg
modified theorem one_sub_invOf_two
modified theorem pos_of_invertible_cast
modified def NonUnitalRingHom.op
modified def NonUnitalRingHom.unop
modified def RingHom.op
modified def RingHom.unop
modified def ULift.ringEquiv
modified theorem RingTopology.ext
modified structure RingTopology
modified theorem mulLeft_continuous
modified theorem mulRight_continuous