Theorem RingHom.CodescendsAlong.algebraMap_tensorProduct

Modification history

2025-07-24 07:37
Mathlib/RingTheory/RingHomProperties.lean
feat(AlgebraicGeometry): codescent implies descent (#23547) …
Added RingHom.CodescendsAlong.algebraMap_tensorProductView on Github →