Commit 2024-09-04 06:34 f760ba9e

View on Github →

chore(RingTheory/TensorProduct/Basic): Remove deprecated lemma (#16468) This was the only lemma needing the LinearAlgebra.FiniteDimensional.Defs import. Came up on Zulip

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

deleted theorem Subalgebra.finiteDimensional_sup