Theorem Subalgebra.tmul_mem_baseChange

Modification history

2025-11-13 13:13
Mathlib/RingTheory/TensorProduct/Maps.lean
feat: define geometrically reduced algebras (#27400) …
Added Subalgebra.tmul_mem_baseChangeView on Github →