mathlib
7aac545b - chore(linear_algebra/dimension): remove unecessary `nontrivial` argument (#18725)

Commit

2 years ago

chore(linear_algebra/dimension): remove unecessary `nontrivial` argument (#18725) This is implied by another hypothesis via `nontrivial_of_invariant_basis_number`

Author

eric-wieser

Parents

08a4542b

mathlib 7aac545b - chore(linear_algebra/dimension): remove unecessary `nontrivial` argument (#18725)

mathlib
7aac545b - chore(linear_algebra/dimension): remove unecessary `nontrivial` argument (#18725)