Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finite_dimensional.of_subalgebra_to_submodule

Modification history

2022-11-19 17:26
src/ring_theory/adjoin/field.lean
feat(linear_algebra/finite_dimensional): generalize from field to division_ring and more (#17401) …
Deleted finite_dimensional.of_subalgebra_to_submoduleView on Github →
2022-11-09 06:40
src/field_theory/splitting_field.lean
chore(field_theory): move `polynomial.splits` to a new file (#17354) …
Modified finite_dimensional.of_subalgebra_to_submoduleView on Github →
2021-03-24 13:49
src/field_theory/splitting_field.lean
chore(algebra/algebra/subalgebra): Add missing coe_sort for subalgebra (#6800) …
Added finite_dimensional.of_subalgebra_to_submoduleView on Github →