Commit 2024-04-11 19:11 aa0ec8aa

View on Github →

feat: add Subalgebra.finite_(bot|sup) (#12025) ... and deprecated Subalgebra.finiteDimensional_(bot|sup)

Estimated changes

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

added theorem Subalgebra.finiteDimensional_bot

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Subalgebra.finite_sup