Theorem surjective_algebraMap_of_linearMap

Modification history

2025-02-03 14:49
Mathlib/Algebra/Algebra/Basic.lean
feat: generalise `algebraMap_injective` by weakening its typeclass assumptions (#21287) …
Modified surjective_algebraMap_of_linearMapView on Github →
2024-05-24 11:39
Mathlib/Algebra/Algebra/Basic.lean
feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot (#12849) …
Added surjective_algebraMap_of_linearMapView on Github →