Theorem Subalgebra.finite_sup

Modification history

2024-11-05 12:09

Mathlib/RingTheory/TensorProduct/Basic.lean

chore(RingTheory/TensorProduct): split finite/free results into new files (#18653)

Modified Subalgebra.finite_sup View on Github →

2024-04-22 02:54

Mathlib/RingTheory/TensorProduct/Basic.lean

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

Modified Subalgebra.finite_sup View on Github →

2024-04-11 19:11

Mathlib/RingTheory/TensorProduct/Basic.lean

feat: add `Subalgebra.finite_(bot|sup)` (#12025) …

Added Subalgebra.finite_sup View on Github →