LinearAlgebra

📁 Source: Mathlib/Algebra/Category/Ring/LinearAlgebra.lean

Statistics

Metric	Count
Definitions	0
Theorems nontrivial_of_isPushout_of_isField	1
Total	1

CommRingCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nontrivial_of_isPushout_of_isField 📖	mathematical	IsField carrier CommSemiring.toSemiring CommRing.toCommSemiring commRing CategoryTheory.IsPushout CommRingCat instCategory	Nontrivial	—	Equiv.nontrivial Module.FaithfullyFlat.lTensor_nontrivial Module.FaithfullyFlat.instOfNontrivialOfFree Module.Free.of_divisionRing

---

← Back to Index