Theorem Module.Baer.ExtensionOf.ext_iff

Modification history

2025-02-11 00:27

Mathlib/Algebra/Module/Injective.lean

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

Deleted Module.Baer.ExtensionOf.ext_iff View on Github →

2023-05-11 14:58

Mathlib/Algebra/Module/Injective.lean

feat: port Algebra.Module.Injective (#3873)

Added Module.Baer.ExtensionOf.ext_iff View on Github →