Commit 2024-04-22 02:54 b5f6488e

View on Github →

chore(RingTheory/TensorProduct/Basic): relax the condition of Subalgebra.finite_sup to CommSemiring (#12323)

Estimated changes

modified theorem Subalgebra.finite_sup