Commit 2024-07-17 17:39 8d10ce36

View on Github →

feat(Algebra/Algebra/Basic) Extend scalars of linear maps along surjective ring homs. (#14373)

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

added def LinearEquiv.extendScalarsOfSurjective

added theorem LinearEquiv.extendScalarsOfSurjective_apply

added theorem LinearEquiv.extendScalarsOfSurjective_symm

added def LinearMap.extendScalarsOfSurjectiveEquiv

added theorem LinearMap.extendScalarsOfSurjective_apply