Commit 2025-05-15 09:40 9e7d035e

View on Github →

chore: remove @[simp] from lemmas that simp [*] can prove (#24926)

Estimated changes

modified theorem Finset.prod_insert_one
modified theorem Cubic.degree_of_a_ne_zero'
modified theorem Cubic.degree_of_b_ne_zero'
modified theorem Cubic.degree_of_c_ne_zero'
modified theorem Cubic.degree_of_d_ne_zero'
modified theorem Commute.pow_pow
modified theorem mul_inv_cancel₀
modified theorem div_mul_cancel₀
modified theorem sq_eq_sq₀
modified theorem Nonneg.pow_nonneg
modified theorem ciInf_pos
modified theorem ciSup_pos