Commit 2025-02-11 00:27 bf839e1c

View on Github →

chore: provide non-dependent versions of LinearPMap.ext and ExtensionOf.ext (#21630)

Estimated changes

Modified Mathlib/Algebra/Module/Injective.lean

added theorem Module.Baer.ExtensionOf.dExt

added theorem Module.Baer.ExtensionOf.dExt_iff

deleted theorem Module.Baer.ExtensionOf.ext_iff

Modified Mathlib/LinearAlgebra/LinearPMap.lean

added theorem LinearPMap.dExt

added theorem LinearPMap.dExt_iff

Modified Mathlib/Topology/Algebra/Module/LinearPMap.lean