Commit 2025-10-14 04:17 91f98c43

View on Github →

feat: group instances on Colex α (#30483) This is just copy-paste + replace Lex with Colex throughout.

Estimated changes

added theorem ofColex_div
added theorem ofColex_eq_one
added theorem ofColex_inv
added theorem ofColex_mul
added theorem ofColex_one
added theorem ofColex_pow
modified theorem ofLex_eq_one
added theorem pow_ofColex
added theorem pow_toColex
added theorem toColex_div
added theorem toColex_eq_one
added theorem toColex_inv
added theorem toColex_mul
added theorem toColex_one
added theorem toColex_pow
modified theorem toLex_eq_one