RightExactness

📁 Source: Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

Statistics

Metric	Count
Definitions equiv, inverse, inverse_of_rightInverse, linearEquiv_of_rightInverse, toFun, equiv, inverse, inverse_of_rightInverse, linearEquiv_of_rightInverse, toFun	10
Theorems lTensor_ker, map_ker, map_surjective, rTensor_ker, map_includeLeft_eq, map_includeRight_eq, ker_tensorProductMk, lTensor_range, lTensor_surjective, rTensor_exact_iff_lTensor_exact, rTensor_range, rTensor_surjective, map_ker, map_surjective, inverse_apply, inverse_comp_lTensor, inverse_of_rightInverse_apply, inverse_of_rightInverse_comp_lTensor, lTensor_exact, lTensor_mkQ, le_comap_range_lTensor, le_comap_range_rTensor, inverse_apply, inverse_comp_rTensor, inverse_of_rightInverse_apply, inverse_of_rightInverse_comp_rTensor, rTensor_exact, rTensor_mkQ	28
Total	38

Algebra.TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lTensor_ker 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	RingHom.ker TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.toDistribMulAction AlgHomClass.toRingHomClass AlgHom.algHomClass map AlgHom.id Ideal.map instAlgebra includeRight	—	IsScalarTower.to_smulCommClass IsScalarTower.left AlgHomClass.toRingHomClass AlgHom.algHomClass IsScalarTower.right RingHomSurjective.ids Ideal.map_includeRight_eq Function.Exact.linearMap_ker_eq lTensor_exact LinearMap.exact_subtype_ker_map
map_ker 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	RingHom.ker TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass map Ideal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Semiring.toModule Ideal.map includeLeft instAlgebra includeRight	—	IsScalarTower.to_smulCommClass ext TensorProduct.isScalarTower_left AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instRingHomClass RingHom.comap_ker IsScalarTower.left lTensor_ker RingHom.ker_eq_comap_bot Ideal.comap_map_of_surjective LinearMap.lTensor_surjective rTensor_ker Ideal.map_map AlgHom.comp_toRingHom map_comp_includeLeft
map_surjective 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring map	—	TensorProduct.map_surjective LinearMap.IsScalarTower.compatibleSMul
rTensor_ker 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	RingHom.ker TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass map AlgHom.id Ideal.map includeLeft	—	IsScalarTower.to_smulCommClass AlgHomClass.toRingHomClass AlgHom.algHomClass IsScalarTower.right RingHomSurjective.ids Ideal.map_includeLeft_eq Function.Exact.linearMap_ker_eq rTensor_exact LinearMap.exact_subtype_ker_map

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_includeLeft_eq 📖	mathematical	—	Submodule.restrictScalars TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring CommSemiring.toSemiring TensorProduct.instModule Semiring.toModule TensorProduct.instSMul IsScalarTower.right Algebra.TensorProduct.instAlgebra map AlgHom Algebra.TensorProduct.leftAlgebra AlgHom.funLike Algebra.TensorProduct.includeLeft LinearMap.range Submodule SetLike.instMembership Submodule.setLike Algebra.toSMul Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid RingHom.id RingHomSurjective.ids LinearMap.rTensor Submodule.subtype	—	IsScalarTower.right RingHomSurjective.ids SetLike.coe_set_eq le_antisymm Submodule.span_induction Set.image_congr map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass TensorProduct.induction_on Algebra.to_smulCommClass MulZeroClass.zero_mul MulZeroClass.mul_zero smul_add add_smul submodule_span_eq map.eq_1 ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass one_mul mul_one mul_mem_left mem_map_of_mem Submodule.coe_mem Submodule.add_mem
map_includeRight_eq 📖	mathematical	—	Submodule.restrictScalars TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring CommSemiring.toSemiring TensorProduct.instModule Semiring.toModule TensorProduct.instSMul IsScalarTower.right Algebra.TensorProduct.instAlgebra map AlgHom AlgHom.funLike Algebra.TensorProduct.includeRight LinearMap.range Submodule SetLike.instMembership Submodule.setLike Algebra.toSMul Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid RingHom.id RingHomSurjective.ids LinearMap.lTensor Submodule.subtype	—	IsScalarTower.right RingHomSurjective.ids SetLike.coe_set_eq le_antisymm Submodule.span_induction Set.image_congr map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass TensorProduct.induction_on Algebra.to_smulCommClass MulZeroClass.zero_mul MulZeroClass.mul_zero smul_add add_smul submodule_span_eq map.eq_1 ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass mul_one one_mul mul_mem_left mem_map_of_mem Submodule.coe_mem Submodule.add_mem

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_tensorProductMk 📖	mathematical	—	ker TensorProduct CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing AddCommGroup.toAddCommMonoid Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap addCommMonoid module TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid instFunLike Ideal.Quotient.one Submodule Submodule.instSMul IsScalarTower.left Top.top Submodule.instTop	—	Submodule.comap_injective_of_surjective RingHomSurjective.ids RingHomInvPair.ids LinearEquiv.surjective TensorProduct.smulCommClass_left smulCommClass_self IsScalarTower.left RingHomCompTriple.ids ker_comp TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.right TensorProduct.isScalarTower Submodule.Quotient.isScalarTower ext_ring IsScalarTower.to_smulCommClass ext one_smul map_one Ideal.instIsTwoSided_1 MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHomSurjective.invPair Submodule.comap_equiv_eq_map_symm Submodule.map_symm_eq_iff Submodule.map_range_rTensor_subtype_lid rTensor_mkQ
lTensor_range 📖	mathematical	—	range TensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lTensor Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.subtype	—	RingHomSurjective.ids RingHomCompTriple.ids lTensor_comp range_comp_of_range_eq_top range_eq_top lTensor_surjective range_rangeRestrict
lTensor_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule lTensor	—	TensorProduct.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass map_add SemilinearMapClass.toAddHomClass
rTensor_exact_iff_lTensor_exact 📖	mathematical	—	Function.Exact TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule instFunLike rTensor TensorProduct.zero lTensor	—	Function.Exact.iff_of_ladder_linearEquiv TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower RingHomCompTriple.ids RingHomInvPair.ids ext IsScalarTower.to_smulCommClass
rTensor_range 📖	mathematical	—	range TensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids rTensor Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.subtype	—	RingHomSurjective.ids RingHomCompTriple.ids rTensor_comp range_comp_of_range_eq_top range_eq_top rTensor_surjective range_rangeRestrict
rTensor_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule rTensor	—	TensorProduct.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass map_add SemilinearMapClass.toAddHomClass

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_ker 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LinearMap.ker TensorProduct addCommMonoid instModule map Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice LinearMap.range RingHomSurjective.ids LinearMap.lTensor LinearMap.rTensor	—	RingHomSurjective.ids RingHomCompTriple.ids LinearMap.lTensor_comp_rTensor LinearMap.ker_comp Function.Exact.linearMap_ker_eq rTensor_exact Submodule.comap_map_eq LinearMap.range_eq_map Submodule.map_comp LinearMap.rTensor_comp_lTensor Submodule.map_top LinearMap.range_eq_top LinearMap.rTensor_surjective lTensor_exact
map_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	TensorProduct addCommMonoid instModule map	—	RingHomCompTriple.ids LinearMap.lTensor_comp_rTensor LinearMap.coe_comp LinearMap.lTensor_surjective LinearMap.rTensor_surjective

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lTensor_exact 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.lTensor TensorProduct.zero	—	RingHomSurjective.ids LinearMap.exact_iff Submodule.ker_mkQ RingHomCompTriple.ids lTensor.inverse_comp_lTensor symm IsEquiv.toSymm eq_isEquiv LinearMap.ker_comp_of_ker_eq_bot LinearMap.ker_eq_bot LinearEquiv.injective RingHomInvPair.ids
lTensor_mkQ 📖	mathematical	—	LinearMap.ker TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid HasQuotient.Quotient Submodule Ring.toSemiring CommRing.toRing Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring LinearMap.lTensor Submodule.mkQ LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids Submodule.subtype	—	RingHomSurjective.ids LinearMap.exact_iff lTensor_exact LinearMap.exact_subtype_mkQ Submodule.mkQ_surjective
le_comap_range_lTensor 📖	mathematical	—	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.comap TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid LinearMap.instFunLike LinearMap.lTensor	—	RingHomSurjective.ids TensorProduct.smulCommClass_left smulCommClass_self
le_comap_range_rTensor 📖	mathematical	—	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.comap TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.smulCommClass_left smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.instFunLike LinearMap.flip LinearMap.rTensor	—	RingHomSurjective.ids SMulCommClass.symm TensorProduct.smulCommClass_left smulCommClass_self
rTensor_exact 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.rTensor TensorProduct.zero	—	LinearMap.rTensor_exact_iff_lTensor_exact lTensor_exact
rTensor_mkQ 📖	mathematical	—	LinearMap.ker TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid HasQuotient.Quotient Submodule Ring.toSemiring CommRing.toRing Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring LinearMap.rTensor Submodule.mkQ LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids Submodule.subtype	—	RingHomSurjective.ids LinearMap.exact_iff rTensor_exact LinearMap.exact_subtype_mkQ Submodule.mkQ_surjective

lTensor

Definitions

Name	Category	Theorems
equiv 📖	CompOp	—
inverse 📖	CompOp	2 math math: inverse_comp_lTensor, inverse_apply
inverse_of_rightInverse 📖	CompOp	2 math math: inverse_of_rightInverse_comp_lTensor, inverse_of_rightInverse_apply
linearEquiv_of_rightInverse 📖	CompOp	—
toFun 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverse_apply 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	TensorProduct HasQuotient.Quotient Submodule TensorProduct.addCommMonoid TensorProduct.instModule Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range RingHomSurjective.ids LinearMap.lTensor Submodule.Quotient.addCommGroup Submodule.Quotient.module inverse Ring.toSemiring	—	RingHomSurjective.ids inverse.eq_1 inverse_of_rightInverse_apply
inverse_comp_lTensor 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LinearMap.comp TensorProduct HasQuotient.Quotient Submodule TensorProduct.addCommMonoid TensorProduct.instModule Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range RingHomSurjective.ids LinearMap.lTensor Submodule.Quotient.addCommGroup Submodule.Quotient.module RingHomCompTriple.ids inverse Submodule.mkQ Ring.toSemiring	—	RingHomSurjective.ids RingHomCompTriple.ids inverse.eq_1 inverse_of_rightInverse_comp_lTensor
inverse_of_rightInverse_apply 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	TensorProduct HasQuotient.Quotient Submodule TensorProduct.addCommMonoid TensorProduct.instModule Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range RingHomSurjective.ids LinearMap.lTensor Submodule.Quotient.addCommGroup Submodule.Quotient.module inverse_of_rightInverse Ring.toSemiring	—	RingHomSurjective.ids LinearMap.congr_fun RingHomCompTriple.ids TensorProduct.ext' Submodule.Quotient.eq TensorProduct.tmul_sub le_comap_range_lTensor LinearMap.exact_iff LinearMap.mem_ker map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_eq_zero
inverse_of_rightInverse_comp_lTensor 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LinearMap.comp TensorProduct HasQuotient.Quotient Submodule TensorProduct.addCommMonoid TensorProduct.instModule Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range RingHomSurjective.ids LinearMap.lTensor Submodule.Quotient.addCommGroup Submodule.Quotient.module RingHomCompTriple.ids inverse_of_rightInverse Submodule.mkQ Ring.toSemiring	—	RingHomSurjective.ids RingHomCompTriple.ids LinearMap.ext_iff inverse_of_rightInverse_apply

rTensor

Definitions

Name	Category	Theorems
equiv 📖	CompOp	—
inverse 📖	CompOp	2 math math: inverse_comp_rTensor, inverse_apply
inverse_of_rightInverse 📖	CompOp	2 math math: inverse_of_rightInverse_apply, inverse_of_rightInverse_comp_rTensor
linearEquiv_of_rightInverse 📖	CompOp	—
toFun 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverse_apply 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	TensorProduct HasQuotient.Quotient Submodule TensorProduct.addCommMonoid TensorProduct.instModule Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range RingHomSurjective.ids LinearMap.rTensor Submodule.Quotient.addCommGroup Submodule.Quotient.module inverse Ring.toSemiring	—	RingHomSurjective.ids inverse.eq_1 inverse_of_rightInverse_apply
inverse_comp_rTensor 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LinearMap.comp TensorProduct HasQuotient.Quotient Submodule TensorProduct.addCommMonoid TensorProduct.instModule Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range RingHomSurjective.ids LinearMap.rTensor Submodule.Quotient.addCommGroup Submodule.Quotient.module RingHomCompTriple.ids inverse Submodule.mkQ Ring.toSemiring	—	RingHomSurjective.ids RingHomCompTriple.ids inverse.eq_1 inverse_of_rightInverse_comp_rTensor
inverse_of_rightInverse_apply 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	TensorProduct HasQuotient.Quotient Submodule TensorProduct.addCommMonoid TensorProduct.instModule Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range RingHomSurjective.ids LinearMap.rTensor Submodule.Quotient.addCommGroup Submodule.Quotient.module inverse_of_rightInverse Ring.toSemiring	—	RingHomSurjective.ids LinearMap.congr_fun RingHomCompTriple.ids TensorProduct.ext' Submodule.Quotient.eq TensorProduct.sub_tmul le_comap_range_rTensor LinearMap.exact_iff LinearMap.mem_ker map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_eq_zero
inverse_of_rightInverse_comp_rTensor 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LinearMap.comp TensorProduct HasQuotient.Quotient Submodule TensorProduct.addCommMonoid TensorProduct.instModule Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range RingHomSurjective.ids LinearMap.rTensor Submodule.Quotient.addCommGroup Submodule.Quotient.module RingHomCompTriple.ids inverse_of_rightInverse Submodule.mkQ Ring.toSemiring	—	RingHomSurjective.ids RingHomCompTriple.ids LinearMap.ext_iff inverse_of_rightInverse_apply

---

← Back to Index