Commit 2023-09-14 09:08 22b19e1a

View on Github →

chore: Module.{Free,Finite} instances for ULift (#7135) These carry no data so should be harmless.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension.lean

added theorem rank_ulift

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean

added theorem FiniteDimensional.finrank_ulift

Modified Mathlib/RingTheory/Finiteness.lean