Commit 2023-04-04 07:41 7aac545b

View on Github →

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

Estimated changes

Modified src/algebra/linear_recurrence.lean

Modified src/linear_algebra/dimension.lean

modified theorem dim_fin_fun

modified theorem dim_fun'

modified theorem dim_fun

modified theorem dim_fun_eq_lift_mul

modified theorem dim_pi