Theorem CommRingCat.nontrivial_of_isPushout_of_isField

Modification history

2024-11-04 13:07
Mathlib/Algebra/Category/Ring/LinearAlgebra.lean
feat(AlgebraicGeometry): pre-requisites of description of topological space of pullback (#18255)
Added CommRingCat.nontrivial_of_isPushout_of_isFieldView on Github →