Theorem finite_dimensional.of_finset_basis
Modification history
2022-08-30 13:54
src/linear_algebra/finite_dimensional.lean
chore(analysis, measure_theory): Fix lint (#16216) …
Deleted finite_dimensional.of_finset_basisView on Github →2021-09-07 16:31
src/linear_algebra/finite_dimensional.lean
feat(linear_algebra/finite_dimensional): generalisations to division_ring (#8822) …
Modified finite_dimensional.of_finset_basisView on Github →2021-05-31 21:08
src/linear_algebra/finite_dimensional.lean
feat(data/finset): provide the coercion `finset α → Type*` (#7575) …
Modified finite_dimensional.of_finset_basisView on Github →2021-05-10 07:36
src/linear_algebra/finite_dimensional.lean
refactor(*): bundle `is_basis` (#7496) …
Modified finite_dimensional.of_finset_basisView on Github →2020-10-11 18:49
src/linear_algebra/finite_dimensional.lean
chore(linear_algebra/finite_dimensional): rename `of_finite_basis` (#4562) …
Modified finite_dimensional.of_finset_basisView on Github →