Commit 2025-05-25 18:26 ecd2fdba

View on Github →

chore(Algebra/Notation/Pi): improve variable names (#25040) Stick to using ι for the domain of the functions, M, G for the codomains equipped with a monoid-like or group-like structure, f, g for the functions themselves, α, β for the auxiliary types with no particular structure.

Estimated changes

modified theorem Pi.apply_mulSingle
modified theorem Pi.apply_mulSingle₂
modified def Pi.mulSingle
modified theorem Pi.mulSingle_apply
modified theorem Pi.mulSingle_comm
modified theorem Pi.mulSingle_eq_of_ne'
modified theorem Pi.mulSingle_eq_of_ne
modified theorem Pi.mulSingle_eq_one_iff
modified theorem Pi.mulSingle_eq_same
modified theorem Pi.mulSingle_inj
modified theorem Pi.mulSingle_injective
modified theorem Pi.mulSingle_ne_one_iff
modified theorem Pi.mulSingle_one
modified theorem Pi.mulSingle_op
modified theorem Pi.mulSingle_op₂
modified theorem Function.const_div
modified theorem Function.const_inv
modified theorem Function.const_mul
modified theorem Function.const_one
modified theorem Function.const_pow
modified theorem Pi.comp_one
modified theorem Pi.div_apply
modified theorem Pi.div_comp
modified theorem Pi.div_def
modified theorem Pi.inv_apply
modified theorem Pi.inv_comp
modified theorem Pi.inv_def
modified theorem Pi.mul_apply
modified theorem Pi.mul_comp
modified theorem Pi.mul_def
modified theorem Pi.one_apply
modified theorem Pi.one_comp
modified theorem Pi.one_def
modified theorem Pi.pow_apply
modified theorem Pi.pow_comp
modified theorem Pi.pow_def
modified theorem Matrix.one_eq_pi_single