Commit 2025-03-05 14:00 114b8de5

feat: generalize map_div's type class (#22571) This generalization does not apply cleanly since a theorem that uses map_div' explicitly references an instance for this theorem. Manually fix that reference. This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile. Otherwise, the type class is not being generalized, but can simply be replaced by implicit type class synthesis (or an implicit type class in a variable block being pulled in.)