Theorem TensorProduct.exists_sum_tmul_eq

Modification history

2026-02-13 16:00
Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
feat(RingTheory): `Algebra.FinitePresentation` descends along faithfully flat algebras (#35254) …
Added TensorProduct.exists_sum_tmul_eqView on Github →