Theorem Algebra.IsPushout.equiv_symm_algebraMap_left

Modification history

2025-02-04 06:00
Mathlib/RingTheory/IsTensorProduct.lean
feat(AlgebraicGeometry): integral = universally closed + affine (#19419) …
Added Algebra.IsPushout.equiv_symm_algebraMap_leftView on Github →