Commit 2023-04-06 17:41 5ec62c81

View on Github →

feat(linear_algebra/finrank): generalize finrank to ring in more places (#18716) This replaces [division_ring K] with the first of the following which compiles:

[ring K]
[ring K] [nontrivial K]
[ring K] [strong_rank_condition K] (implies the previous one via the non-instance nontrivial_of_invariant_basis_number)

Estimated changes

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/category_theory/preadditive/schur.lean

Modified src/linear_algebra/eigenspace.lean

Modified src/linear_algebra/finite_dimensional.lean

Modified src/linear_algebra/finrank.lean

modified theorem finite_dimensional.nontrivial_of_finrank_eq_succ

modified theorem finite_dimensional.nontrivial_of_finrank_pos

modified theorem finrank_bot

modified theorem finrank_eq_one

modified theorem subalgebra.finrank_bot

modified theorem subalgebra.rank_bot