Commit 2024-02-15 06:24 2288eab6

View on Github →

chore(LinearAlgebra): golf (#10569)

rename span_eq_top_of_linearIndependent_of_card_eq_finrank to LinearIndependent.span_eq_top_of_card_eq_finrank;
add a version LinearIndependent.span_eq_top_of_card_eq_finrank' with different typeclass assumptions;
use rfl to prove Algebra.discr_def;
golf Algebra.discr_not_zero_of_basis.

Estimated changes

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

added theorem LinearIndependent.span_eq_top_of_card_eq_finrank'

added theorem LinearIndependent.span_eq_top_of_card_eq_finrank

deleted theorem span_eq_top_of_linearIndependent_of_card_eq_finrank

Modified Mathlib/RingTheory/Discriminant.lean

modified theorem Algebra.discr_def