Commit 2023-08-18 21:51 e79a197c

fix(LinearAlgebra/Dimension): make LinearMap.rank an abbrev (#6545) Previously, a statement like:

import Mathlib.LinearAlgebra.Dimension
import Mathlib.Tactic
variable {K : Type} [Field K]
variable {V W : Type} [AddCommGroup V] [AddCommGroup W] [Module K V] [Module K W]
variable {L : V →ₗ[K] W}
open LinearMap (ker)
open Module (rank)
example : rank K V = L.rank + rank K (ker L) := by
    sorry

required rewriting LinearMap.rank before manually finding the existence of rank_range_add_rank_ker. After this change though, exact? successfully finds the lemma / solves the above.