Finite

📁 Source: Mathlib/RingTheory/TensorProduct/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems base_change, tensorProduct, exists_isPrincipal_quotient_of_finite, exists_surjective_quotient_of_finite, tensorProductMap, finite_sup, exists_fg_le_eq_rTensor_inclusion, exists_fg_le_eq_rTensor_subtype, exists_fg_le_subset_range_rTensor_inclusion, exists_fg_le_subset_range_rTensor_subtype, instNontrivialTensorProduct	11
Total	11

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isPrincipal_quotient_of_finite 📖	mathematical	—	Submodule.IsPrincipal HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module Top.top Submodule.instTop	—	Finite.exists_fin lt_iff_not_ge Set.ext LT.lt.trans_le Set.image_univ IsMin.Iio_eq Set.image_empty Submodule.span_empty Submodule.instNontrivial LT.lt.le Nat.sSup_mem notMem_of_csSup_lt Order.lt_succ Nat.instNoMaxOrder Set.image_singleton RingHomSurjective.ids Submodule.map_span Submodule.comap_injective_of_surjective Submodule.mkQ_surjective Submodule.comap_map_eq Submodule.ker_mkQ Submodule.comap_top Submodule.span_union Order.Iio_succ_eq_insert Set.union_singleton Set.preimage_union Set.image_union Set.union_comm
exists_surjective_quotient_of_finite 📖	mathematical	—	HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule LinearMap.instFunLike	—	exists_isPrincipal_quotient_of_finite RingHomInvPair.ids RingHomSurjective.ids LinearMap.range_eq_top LinearMap.span_singleton_eq_range RingHomCompTriple.ids Submodule.Quotient.nontrivial_iff Submodule.span_zero_singleton Submodule.instNontrivial one_smul LinearMap.congr_fun LinearMap.ker_eq_top LinearEquiv.surjective Submodule.mkQ_surjective

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_change 📖	mathematical	—	Module.Finite TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass	—	Algebra.to_smulCommClass fg_top TensorProduct.smulCommClass_left smulCommClass_self eq_top_iff TensorProduct.induction_on ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Finset.coe_image Submodule.span_span_of_tower TensorProduct.isScalarTower_left IsScalarTower.right RingHomSurjective.ids Submodule.span_image Submodule.map_top LinearMap.coe_range mul_one smul_eq_mul TensorProduct.smul_tmul' Submodule.smul_mem Submodule.subset_span Set.mem_range_self Submodule.add_mem
tensorProduct 📖	mathematical	—	Module.Finite TensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule	—	TensorProduct.map₂_mk_top_top_eq_top Submodule.FG.map₂ fg_top

RingHom.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensorProductMap 📖	mathematical	—	RingHom.Finite TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Algebra.TensorProduct.instCommRing AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.TensorProduct.map	—	IsScalarTower.to_smulCommClass IsScalarTower.left AlgHomClass.toRingHomClass AlgHom.algHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Algebra.TensorProduct.ext TensorProduct.isScalarTower AlgHom.ext Algebra.TensorProduct.map_comp_includeLeft map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass TensorProduct.isScalarTower_left Algebra.TensorProduct.map_restrictScalars_comp_includeRight comp RingEquiv.finite

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_sup 📖	mathematical	—	Module.Finite Subalgebra CommSemiring.toSemiring SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toSemiring instModuleSubtypeMem	—	range_val Algebra.TensorProduct.productMap_range Module.Finite.range Module.Finite.tensorProduct

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_fg_le_eq_rTensor_inclusion 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Submodule SetLike.instMembership setLike addCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor inclusion	—	exists_fg_le_eq_rTensor_subtype RingHomSurjective.ids FG.map map_subtype_le RingHomCompTriple.ids LinearMap.rTensor_comp_apply
exists_fg_le_eq_rTensor_subtype 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Submodule SetLike.instMembership setLike addCommMonoid module TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor subtype	—	TensorProduct.induction_on fg_bot fg_span_singleton mem_span_singleton_self FG.sup le_sup_left le_sup_right map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass RingHomCompTriple.ids LinearMap.rTensor_comp_apply
exists_fg_le_subset_range_rTensor_inclusion 📖	mathematical	—	Set TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership setLike addCommMonoid module Set.instHasSubset SetLike.coe TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.rTensor inclusion	—	RingHomSurjective.ids fg_iSup Set.finite_coe_iff iSup_le le_iSup RingHomCompTriple.ids LinearMap.comp_apply LinearMap.rTensor_comp exists_fg_le_eq_rTensor_inclusion
exists_fg_le_subset_range_rTensor_subtype 📖	mathematical	—	Set TensorProduct Set.instHasSubset SetLike.coe Submodule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule setLike LinearMap.range SetLike.instMembership addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.rTensor subtype	—	RingHomSurjective.ids fg_iSup Set.finite_coe_iff le_iSup RingHomCompTriple.ids LinearMap.comp_apply LinearMap.rTensor_comp exists_fg_le_eq_rTensor_subtype

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNontrivialTensorProduct 📖	mathematical	—	Nontrivial TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Module.exists_surjective_quotient_of_finite RingHomCompTriple.ids Ideal.Quotient.smulCommClass Ideal.instIsTwoSided_1 Algebra.to_smulCommClass Ideal.Quotient.isScalarTower_right Submodule.Quotient.nontrivial_iff mul_one Function.Surjective.nontrivial

---

← Back to Index