Bilinear

📁 Source: Mathlib/Algebra/Module/Submodule/Bilinear.lean

Statistics

Metric	Count
Definitions map₂	1
Theorems apply_mem_map₂, image2_subset_map₂, map_map₂, map₂_bot_left, map₂_bot_right, map₂_eq_span_image2, map₂_flip, map₂_iSup_left, map₂_iSup_right, map₂_le, map₂_le_map₂, map₂_le_map₂_left, map₂_le_map₂_right, map₂_map_left, map₂_map_map, map₂_map_right, map₂_span_singleton_eq_map, map₂_span_singleton_eq_map_flip, map₂_span_span, map₂_sup_left, map₂_sup_right	21
Total	22

Submodule

Definitions

Name	Category	Theorems
map₂ 📖	CompOp	28 math math: smul_eq_map₂, TensorProduct.range_mapIncl, map₂_iSup_right, TensorProduct.range_map, map₂_le_map₂, map₂_bot_right, TensorProduct.map₂_eq_range_lift_comp_mapIncl, map₂_iSup_left, map₂_bot_left, map₂_map_left, map₂_map_right, apply_mem_map₂, map₂_eq_span_image2, map₂_span_singleton_eq_map_flip, map₂_span_span, map₂_le, TensorProduct.map₂_mk_top_top_eq_top, map₂_span_singleton_eq_map, map₂_flip, map_map₂, FG.map₂, image2_subset_map₂, map₂_sup_left, mul_eq_map₂, map₂_map_map, map₂_le_map₂_left, map₂_sup_right, map₂_le_map₂_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mem_map₂ 📖	mathematical	Submodule CommSemiring.toSemiring SetLike.instMembership setLike	map₂ DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self le_iSup
image2_subset_map₂ 📖	mathematical	—	Set Set.instHasSubset Set.image2 DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.coe Submodule setLike map₂	—	smulCommClass_self apply_mem_map₂
map_map₂ 📖	mathematical	—	map CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids map₂ LinearMap.compr₂ smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	smulCommClass_self RingHomSurjective.ids IsScalarTower.left map_iSup iSup_congr RingHomCompTriple.ids map_comp
map₂_bot_left 📖	mathematical	—	map₂ Bot.bot Submodule CommSemiring.toSemiring instBot	—	smulCommClass_self eq_bot_iff map₂_le mem_bot LinearMap.map_zero₂
map₂_bot_right 📖	mathematical	—	map₂ Bot.bot Submodule CommSemiring.toSemiring instBot	—	smulCommClass_self eq_bot_iff map₂_le mem_bot map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
map₂_eq_span_image2 📖	mathematical	—	map₂ span CommSemiring.toSemiring Set.image2 DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.coe Submodule setLike	—	smulCommClass_self map₂_span_span span_eq
map₂_flip 📖	mathematical	—	map₂ LinearMap.flip CommSemiring.toSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id Semiring.toNonAssocSemiring	—	smulCommClass_self map₂_eq_span_image2 Set.image2_swap
map₂_iSup_left 📖	mathematical	—	map₂ iSup Submodule CommSemiring.toSemiring ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	smulCommClass_self map₂_span_span Set.image2_iUnion_left span_eq
map₂_iSup_right 📖	mathematical	—	map₂ iSup Submodule CommSemiring.toSemiring ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	smulCommClass_self map₂_span_span Set.image2_iUnion_right span_eq
map₂_le 📖	mathematical	—	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder map₂ SetLike.instMembership setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self apply_mem_map₂ iSup_le map_le_iff_le_comap
map₂_le_map₂ 📖	mathematical	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder	map₂	—	smulCommClass_self map₂_le apply_mem_map₂
map₂_le_map₂_left 📖	mathematical	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder	map₂	—	smulCommClass_self map₂_le_map₂ le_refl
map₂_le_map₂_right 📖	mathematical	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder	map₂	—	smulCommClass_self map₂_le_map₂ le_refl
map₂_map_left 📖	mathematical	—	map₂ map CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.comp LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids	—	smulCommClass_self RingHomSurjective.ids RingHomCompTriple.ids map₂_flip map₂_map_right
map₂_map_map 📖	mathematical	—	map₂ map CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.compl₁₂ smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self RingHomSurjective.ids RingHomCompTriple.ids map₂_map_right map₂_map_left
map₂_map_right 📖	mathematical	—	map₂ map CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.compl₂ RingHomCompTriple.ids smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self iSup_congr RingHomSurjective.ids RingHomCompTriple.ids map_comp
map₂_span_singleton_eq_map 📖	mathematical	—	map₂ span CommSemiring.toSemiring Set Set.instSingletonSet map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike	—	smulCommClass_self RingHomSurjective.ids span_eq map₂_span_span Set.image2_singleton_left map_span
map₂_span_singleton_eq_map_flip 📖	mathematical	—	map₂ span CommSemiring.toSemiring Set Set.instSingletonSet map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids 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 smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.instFunLike LinearMap.flip	—	smulCommClass_self RingHomSurjective.ids SMulCommClass.symm map₂_span_singleton_eq_map map₂_flip
map₂_span_span 📖	mathematical	—	map₂ span CommSemiring.toSemiring Set.image2 DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self le_antisymm map₂_le span_induction subset_span map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass AddSubmonoidClass.toZeroMemClass addSubmonoidClass map_add SemilinearMapClass.toAddHomClass AddSubmonoidClass.toAddMemClass map_smul SemilinearMapClass.toMulActionSemiHomClass span_le Set.image2_subset_iff apply_mem_map₂
map₂_sup_left 📖	mathematical	—	map₂ Submodule CommSemiring.toSemiring SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	smulCommClass_self le_antisymm map₂_le mem_sup apply_mem_map₂ LinearMap.map_add₂ sup_le map₂_le_map₂_left le_sup_left le_sup_right
map₂_sup_right 📖	mathematical	—	map₂ Submodule CommSemiring.toSemiring SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	smulCommClass_self le_antisymm map₂_le mem_sup apply_mem_map₂ map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass sup_le map₂_le_map₂_right le_sup_left le_sup_right

---

← Back to Index