Theorem Algebra.TensorProduct.adjoin_one_tmul_image_eq_top

Modification history

2026-02-06 15:35
Mathlib/RingTheory/TensorProduct/Basic.lean
feat(RingTheory): local structure of monogenic unramified algebras (#33903)
Added Algebra.TensorProduct.adjoin_one_tmul_image_eq_topView on Github →