Basis

📁 Source: Mathlib/RingTheory/Extension/Cotangent/Basis.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_presentation_of_basis_cotangent, exists_presentation_of_free_cotangent	2
Total	2

Algebra.Generators

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_presentation_of_basis_cotangent 📖	mathematical	—	val Algebra.Presentation.toGenerators DFunLike.coe Module.Basis Algebra.Extension.Cotangent toExtension CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id Module.Basis.instFunLike LinearMap Algebra.Extension.Ring Algebra.Extension.commRing RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.Extension.ker Submodule.addCommMonoid Submodule.module Algebra.Extension.algebra₂ LinearMap.instFunLike Algebra.Presentation.relation Algebra.Presentation.relation_mem_ker	—	subsingleton_or_nontrivial Algebra.Presentation.relation_mem_ker Function.surjective_to_subsingleton Set.range_const Ideal.span_singleton_one RingHom.ker_eq_top_of_subsingleton Module.subsingleton AlgHomClass.toRingHomClass AlgHom.algHomClass ker_eq_ker_aeval_val Algebra.FinitePresentation.ker_fG_of_surjective algebraMap_eq algebraMap_surjective Algebra.FinitePresentation.mvPolynomial Algebra.Etale.finitePresentation Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat Algebra.IsStandardSmoothOfRelativeDimension.id IsScalarTower.right Submodule.comap_le_comap_iff_of_le_range RingHomSurjective.ids Submodule.range_subtype Submodule.comap_subtype_self Submodule.comap_sup_of_injective Submodule.subtype_injective IsScalarTower.left Submodule.comap_smul'' Submodule.coe_subtype Ideal.span.eq_1 Set.range_comp Submodule.map_span Submodule.comap_map_eq_of_injective Submodule.isScalarTower' Algebra.Extension.instIsScalarTowerCotangent Submodule.restrictScalars_span le_trans le_top top_le_iff Submodule.restrictScalars_eq_top_iff Module.Basis.span_eq smulCommClass_self Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup le_rfl Algebra.Extension.Cotangent.mk_surjective
exists_presentation_of_free_cotangent 📖	mathematical	—	val Algebra.Presentation.toGenerators Module.finrank Algebra.Extension.Cotangent toExtension CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.Extension.instAddCommGroupCotangent Algebra.Extension.instModuleCotangent Algebra.id DFunLike.coe Module.Basis Module.Basis.instFunLike LinearMap Algebra.Extension.Ring Algebra.Extension.commRing RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.Extension.ker Submodule.addCommMonoid Submodule.module Algebra.Extension.algebra₂ LinearMap.instFunLike Algebra.Presentation.relation Algebra.Presentation.relation_mem_ker	—	subsingleton_or_nontrivial Algebra.Presentation.relation_mem_ker Function.surjective_to_subsingleton Set.range_const Ideal.span_singleton_one RingHom.ker_eq_top_of_subsingleton Module.subsingleton Algebra.Extension.Cotangent.finite fg_ker_of_finitePresentation exists_presentation_of_basis_cotangent commRing_strongRankCondition

---

← Back to Index