Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alg_hom.bijective

Modification history

2022-08-11 16:08
src/linear_algebra/finite_dimensional.lean
feat(ring_theory/algebraic): `alg_hom` from an algebraic extension to itself is bijective (#15873) …
Modified alg_hom.bijectiveView on Github →
2020-10-29 09:49
src/linear_algebra/finite_dimensional.lean
feat(linear_algebra/finite_dimensional): finite dimensional algebra_hom of fields is bijective (#4793) …
Added alg_hom.bijectiveView on Github →