Theorem bijective_algebraMap_of_linearEquiv

Modification history

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