Skip to content

Commit

Permalink
feat: port LinearAlgebra.Finrank (#3378)
Browse files Browse the repository at this point in the history
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: EmilieUthaiwat <emiliepathum@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
13 people committed Apr 12, 2023
1 parent 0ae830f commit 1e02adb
Show file tree
Hide file tree
Showing 2 changed files with 586 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Expand Up @@ -1268,6 +1268,7 @@ import Mathlib.LinearAlgebra.Dfinsupp
import Mathlib.LinearAlgebra.Dimension
import Mathlib.LinearAlgebra.DirectSum.Finsupp
import Mathlib.LinearAlgebra.DirectSum.TensorProduct
import Mathlib.LinearAlgebra.Finrank
import Mathlib.LinearAlgebra.Finsupp
import Mathlib.LinearAlgebra.FinsuppVectorSpace
import Mathlib.LinearAlgebra.FreeAlgebra
Expand Down

0 comments on commit 1e02adb

Please sign in to comment.