Theorem injective_algebraMap_of_linearMap

Modification history

2024-05-24 11:39
Mathlib/Algebra/Algebra/Basic.lean
feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot (#12849) …
Added injective_algebraMap_of_linearMapView on Github →