Commit 2026-10-13 20:38 8084bdcf

View on Github →

refactor(Algebra): make the arguments of Is*Apply implicit (#42704) Since IsAddApply F α β and similar classes have [FunLike F α β] as an assumption, α and β can always be inferred from F, so they can be made implicit.

Estimated changes

modified theorem FunLike.coe_div
modified theorem FunLike.coe_intCast
modified theorem FunLike.coe_inv
modified theorem FunLike.coe_mul
modified theorem FunLike.coe_mul_eq_comp
modified theorem FunLike.coe_natCast
modified theorem FunLike.coe_one
modified theorem FunLike.coe_one_eq_id
modified theorem FunLike.coe_one_eq_id_iff
modified theorem FunLike.coe_one_iff
modified theorem FunLike.coe_pow
modified theorem FunLike.coe_pow_eq_iterate
modified theorem pow_apply_eq_iterate