TotallySplit

📁 Source: Mathlib/RingTheory/TotallySplit.lean

Statistics

Metric	Count
Definitions IsFiniteSplit	1
Theorems inst, instEtale, instFinitePresentation, instForallOfFinite, instFree, instTensorProduct, nonempty_algEquiv_fun, of_algEquiv, of_subsingleton	9
Total	10

Algebra

Definitions

Name	Category	Theorems
IsFiniteSplit 📖	CompData	5 math math: IsFiniteSplit.of_subsingleton, IsFiniteSplit.instForallOfFinite, IsFiniteSplit.of_algEquiv, IsFiniteSplit.instTensorProduct, IsFiniteSplit.inst

Algebra.IsFiniteSplit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inst 📖	mathematical	—	Algebra.IsFiniteSplit Algebra.id CommRing.toCommSemiring	—	of_algEquiv instForallOfFinite Finite.of_fintype
instEtale 📖	mathematical	—	Algebra.Etale	—	nonempty_algEquiv_fun Algebra.Etale.of_equiv Algebra.FormallyEtale.instEtaleForallOfFinite Finite.of_fintype Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat Algebra.IsStandardSmoothOfRelativeDimension.id
instFinitePresentation 📖	mathematical	—	Module.FinitePresentation CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	—	nonempty_algEquiv_fun Module.FinitePresentation.of_equiv Module.FinitePresentation.pi instFinitePresentation Finite.of_fintype
instForallOfFinite 📖	mathematical	—	Algebra.IsFiniteSplit Pi.commRing Function.algebra CommRing.toCommSemiring Ring.toSemiring CommRing.toRing Algebra.id	—	nonempty_fintype
instFree 📖	mathematical	—	Module.Free CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	—	nonempty_algEquiv_fun Module.Free.of_equiv RingHomInvPair.ids Module.Free.function Finite.of_fintype Module.Free.self
instTensorProduct 📖	mathematical	—	Algebra.IsFiniteSplit TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass nonempty_algEquiv_fun IsScalarTower.to_smulCommClass IsScalarTower.right
nonempty_algEquiv_fun 📖	mathematical	—	AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring Pi.semiring Function.algebra Algebra.id	—	—
of_algEquiv 📖	mathematical	—	Algebra.IsFiniteSplit	—	nonempty_algEquiv_fun
of_subsingleton 📖	mathematical	—	Algebra.IsFiniteSplit	—	RingHom.codomain_trivial

---

← Back to Index