mathlib

1a424e18 - chore(number_theory/modular): add missing lemmas to squeeze simps (#15351)

chore(number_theory/modular): add missing lemmas to squeeze simps (#15351) I was running into some timeouts in `exists_smul_mem_fd` when making some other changes; this extracts some `simp` calls to standalone lemmas. These lemmas don't have particularly fast proofs either, but the statements are much simpler so will be easier to speed up in future if we need to. Simp-normal form in this file seems to aggressively unfold to matrices, so we can't mark these new lemmas `simp`. At some point the simp lemmas for modular forms might want to be revisited.