Commit 2024-11-25 09:33 f801de49

View on Github →

chore: split notation typeclasses out of Algebra.Group.Defs (#19350)

Estimated changes

deleted theorem SMul.smul_eq_hSMul
deleted theorem dite_div
deleted theorem dite_div_dite
deleted theorem dite_mul
deleted theorem dite_mul_dite
deleted theorem div_dite
deleted theorem div_ite
deleted theorem ite_div
deleted theorem ite_div_ite
deleted theorem ite_mul
deleted theorem ite_mul_ite
deleted theorem mul_dite
deleted theorem mul_ite
added theorem SMul.smul_eq_hSMul
added theorem dite_div
added theorem dite_div_dite
added theorem dite_mul
added theorem dite_mul_dite
added theorem div_dite
added theorem div_ite
added theorem ite_div
added theorem ite_div_ite
added theorem ite_mul
added theorem ite_mul_ite
added theorem mul_dite
added theorem mul_ite