Commit 2024-06-20 16:11 d48b0c68

View on Github →

chore: drop porting notes about nonrec (#13767)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added theorem AlgEquiv.map_finsupp_prod

added theorem AlgEquiv.map_prod

Modified Mathlib/LinearAlgebra/Span.lean

added theorem Submodule.prod_mono