Commit 2025-12-09 23:13 0c25ddf8

View on Github →

chore: golf using grind and simp (#32656)

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/LinearAlgebra/LinearPMap.lean

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

modified theorem Submodule.Quotient.nontrivial_of_lt_top

modified theorem Submodule.Quotient.nontrivial_of_ne_top