BilinearMap

📁 Source: Mathlib/LinearAlgebra/BilinearMap.lean

Statistics

Metric	Count
Definitions BilinForm, BilinMap, compl₁₂, compl₂, compr₂, compr₂ₛₗ, domRestrict₁₂, domRestrict₂, flip, lcomp, lcompₛₗ, lflip, llcomp, lsmul, mk₂, mk₂', mk₂'ₛₗ, restrictScalarsRange, restrictScalarsRange₂, restrictScalars₁₂	20
Theorems bijective_compr₂_of_equiv, bijective_compr₂ₛₗ_of_equiv, compl₁₂_apply, compl₁₂_id_id, compl₁₂_inj, compl₂_apply, compl₂_id, compr₂_apply, compr₂ₛₗ_apply, congr_fun₂, domRestrict₁₂_apply, domRestrict₂_apply, eq_restrictScalarsRange_iff, eq_restrictScalarsRange₂_iff, ext_iff₂, ext₂, flip_apply, flip_flip, flip_inj, injective_compr₂_of_injective, injective_compr₂ₛₗ_of_injective, ker_lsmul, lcomp_apply, lcomp_apply', lcomp_injective_of_surjective, lcompₛₗ_apply, lflip_apply, lflip_symm, llcomp_apply, llcomp_apply', lsmul_apply, lsmul_eq_DistribMulAction_toLinearMap, lsmul_eq_distribSMultoLinearMap, lsmul_injective, map_add₂, map_neg₂, map_smul₂, map_smulₛₗ₂, map_sub₂, map_sum₂, map_zero₂, mk₂'_apply, mk₂'ₛₗ_apply, mk₂_apply, restrictScalarsRange_apply, restrictScalarsRange_apply_eq_zero_iff, restrictScalarsRange₂_apply, restrictScalarsRange₂_apply_eq_zero_iff, restrictScalars₁₂_apply_apply, restrictScalars₁₂_inj, restrictScalars₁₂_injective, surjective_compr₂_of_equiv, surjective_compr₂_of_exists_rightInverse, surjective_compr₂ₛₗ_of_equiv, surjective_compr₂ₛₗ_of_exists_rightInverse	55
Total	75

LinearMap

Definitions

Name	Category	Theorems
BilinForm 📖	CompOp	275 math math: RootPairing.InvariantForm.apply_reflection_reflection, RootPairing.rootForm_self_smul_coroot, RootPairing.RootPositiveForm.algebraMap_rootLength, BilinForm.dualSubmoduleParing_spec, BilinForm.zero_right, Matrix.SeparatingLeft.toBilin', RootPairing.posRootForm_posForm_apply_apply, RootPairing.four_nsmul_coPolarization_compl_polarization_apply_root, BilinForm.toMatrix_toBilin, BilinForm.symmCompOfNondegenerate_left_apply, BilinForm.toMatrix_symm, RootPairing.coroot_eq_polarizationEquiv_apply_root, CliffordAlgebra.changeForm_comp_changeForm, RootPairing.RootPositiveForm.zero_lt_posForm_apply_root, BilinForm.IsAlt.neg_eq, BilinForm.toMatrixAux_eq, BilinForm.smul_left_of_tower, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, LieModule.traceForm_eq_sum_genWeightSpaceOf, RootPairing.EmbeddedG2.shortAddLongRoot_shortRoot, BilinForm.congr_apply, BilinForm.toMatrix_compRight, ContinuousLinearMap.toBilinForm_apply, BilinForm.IsNonneg.nonneg, Matrix.separatingRight_toBilin_iff, RootPairing.InvariantForm.pairing_mul_eq_pairing_mul_swap, BilinForm.toMatrix'_symm, BilinForm.IsRefl.groupSMul, BilinForm.toMatrix'_apply, BilinForm.SeparatingRight.toMatrix, RootPairing.coPolarization_apply_eq_zero_iff, Matrix.toBilin_symm, Algebra.traceMatrix_apply, BilinForm.sum_right, RootPairing.RootPositiveForm.zero_lt_posForm_iff, RootPairing.toLinearMap_apply_CoPolarization, BilinForm.ext_iff_of_isSymm, CliffordAlgebra.changeForm_self_apply, BilinForm.IsAlt.eq_of_add_add_eq_zero, CliffordAlgebra.changeFormAux_changeFormAux, BilinForm.nondegenerate_toMatrix_iff, CliffordAlgebra.changeForm.add_proof, LieModule.traceForm_eq_zero_of_isNilpotent, BilinForm.sub_left, Matrix.toBilin_apply, BilinForm.coeFnAddMonoidHom_apply, Matrix.nondegenerate_toBilin'_iff, BilinForm.congr_comp, Algebra.traceForm_apply, CliffordAlgebra.changeFormEquiv_symm, BilinForm.apply_dualBasis_left, CliffordAlgebra.changeForm.zero_proof, RootPairing.exists_ge_zero_eq_rootForm, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, BilinForm.isNonneg_def, RootPairing.RootPositiveForm.posForm_apply_root_root_le_zero_iff, LieIdeal.mem_killingCompl, BilinForm.sum_left, RootPairing.toLinearMap_apply_apply_Polarization, BilinForm.Nondegenerate.congr, BilinForm.separatingLeft_toMatrix'_iff, BilinForm.not_nondegenerate_zero, BilinForm.IsSymm.eq, BilinForm.mul_toMatrix'_mul, BilinForm.mul_toMatrix_mul, CliffordAlgebra.changeForm_ι_mul, LieModule.traceForm_lieSubalgebra_mk_right, CliffordAlgebra.changeForm_self, RootPairing.RootPositiveForm.exists_eq, toBilin'Aux_toMatrixAux, RootPairing.rootForm_root_self, BilinForm.isRefl_zero, BilinForm.tensorDistribEquiv_toLinearMap, Algebra.traceForm_toMatrix, toBilin'Aux_toMatrixAux, BilinForm.dotProduct_toMatrix_mulVec, BilinForm.tensorDistrib_tmul, RootPairing.InvariantForm.exists_apply_eq_or, BilinForm.compLeft_injective, RootPairing.zero_le_rootForm, BilinForm.smul_right_of_tower, BilinForm.tensorDistribEquiv_apply, BilinForm.toMatrix_apply, LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero, BilinForm.toMatrix_toBilin, BilinForm.IsRefl.smul, BilinForm.IsNonneg.add, BilinForm.IsPosSemidef.smul, killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting, BilinForm.add_left, RootPairing.toLinearMap_apply_PolarizationIn, BilinForm.separatingRight_toMatrix'_iff, RootPairing.EmbeddedG2.long_eq_three_mul_short, BilinForm.smul_left, BilinForm.lieInvariant_iff, BilinForm.dotProduct_toMatrix_mulVec, LieModule.traceForm_comm, Matrix.toBilin'_symm, BilinForm.isSymm_iff_flip, RootPairing.corootForm_apply_apply, BilinForm.mem_dualSubmodule, BilinForm.toMatrix_comp, BilinForm.neg_left, BilinForm.sum_repr_mul_repr_mul, Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin, BilinForm.IsAlt.self_eq_zero, BilinearForm.toMatrixAux_eq, RootPairing.rootForm_reflection_reflection_apply, RootPairing.posRootForm_posForm_pos_of_ne_zero, Matrix.SeparatingLeft.toBilin, BilinForm.IsPosSemidef.add, BilinForm.zero_left, Matrix.nondegenerate_toBilin_iff, BilinForm.isSymm_neg, BilinForm.toDual_def, BilinForm.toMatrix'_compLeft, BilinForm.dualBasis_repr_apply, Matrix.Nondegenerate.toBilin, BilinForm.nondegenerate_toBilin'_iff_det_ne_zero, BilinForm.separatingRight_toMatrix_iff, RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict, BilinForm.SeparatingLeft.toMatrix', BilinForm.zero_apply, RootPairing.algebraMap_rootFormIn, BilinForm.isNonneg_zero, BilinForm.IsSymm.sub, CliffordAlgebra.changeForm_ι_mul_ι, RootPairing.rootForm_self_eq_zero_iff, BilinForm.dualBasis_eq_iff, Matrix.toBilin'Aux_single, LieModule.lie_traceForm_eq_zero, FractionalIdeal.mem_dual, RootPairing.zero_le_posForm, BilinForm.sub_apply, killingForm_apply_apply, BilinForm.congr_refl, RootPairing.InvariantForm.apply_weylGroup_smul, BilinForm.toMatrix_symm, BilinForm.SeparatingLeft.toMatrix, RootPairing.rootForm_apply_apply, LieModule.traceForm_eq_zero_of_isTrivial, BilinForm.IsSymm.smul, BilinForm.toMatrix_compRight, BilinForm.nondegenerate_toMatrix'_iff, BilinForm.congr_congr, BilinForm.isAlt_zero, BilinForm.toMatrixAux_apply, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, BilinForm.toLin'Flip_apply, BilinForm.toMatrix_mul_basis_toMatrix, BilinForm.mul_toMatrix', BilinForm.IsRefl.neg, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs, BilinForm.IsSymm.add, BilinForm.isAlt_neg, BilinForm.ext_iff, RootPairing.RootPositiveForm.two_mul_apply_root_root, Matrix.toBilin'_apply, RootPairing.prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, RootPairing.rootForm_self_sum_of_squares, BilinForm.isRefl_neg, RootPairing.algebraMap_posRootForm_posForm, BilinForm.nondegenerate_congr_iff, BilinForm.flip_apply, BilinForm.compRight_apply, Algebra.traceMatrix_of_basis, LieModule.traceForm_lieSubalgebra_mk_left, CliffordAlgebra.changeForm.neg_proof, BilinForm.IsSymm.neg, BilinForm.add_right, Matrix.toBilin_toMatrix, BilinForm.comp_congr, Matrix.toBilin'_comp, RootPairing.InvariantForm.apply_eq_or_aux, LieAlgebra.InvariantForm.mem_orthogonal, BilinForm.tensorDistribEquiv_tmul, BilinForm.mul_toMatrix_mul, BilinForm.toMatrix_mul_basis_toMatrix, BilinForm.toMatrix'_comp, ContinuousLinearMap.toBilinForm_injective, BilinForm.IsAlt.neg, BilinForm.toMatrix_mul, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, BilinForm.toMatrix_compLeft, RootPairing.polarizationEquiv_symm_apply_coroot, BilinForm.toMatrix_apply, Matrix.toBilin'_apply', BilinForm.IsSymm.polarization, BilinForm.mul_toMatrix, BilinForm.flip_flip, BilinForm.toMatrix_mul, RootPairing.RootPositiveForm.exists_pos_eq, Matrix.separatingLeft_toBilin'_iff, BilinForm.isSymm_def, Matrix.toBilin'Aux_eq, Submodule.mem_traceDual, BilinForm.isSymm_zero, BilinForm.coe_injective, BilinForm.smul_right, LieModule.traceForm_genWeightSpace_eq, LieModule.traceForm_apply_apply, RootPairing.rootFormIn_self_smul_coroot, RootPairing.corootForm_self_smul_root, RootPairing.exists_form_eq_form_and_form_ne_zero, Matrix.separatingRight_toBilin'_iff, RootPairing.InvariantForm.apply_root_root_zero_iff, BilinForm.apply_toDual_symm_apply, BilinForm.neg_apply, RootPairing.rootForm_pos_of_ne_zero, BilinForm.isPosSemidef_zero, LieModule.traceForm_apply_lie_apply, BilinForm.compLeft_apply, BilinForm.mul_toMatrix, RootPairing.RootPositiveForm.algebraMap_apply_eq_form_iff, RootPairing.InvariantForm.apply_eq_or, Matrix.Nondegenerate.toBilin', BilinForm.congr_trans, BilinForm.toMatrix'_mul, LieAlgebra.IsKilling.traceForm_coroot, BilinForm.comp_apply, Module.Basis.traceDual_repr_apply, LieModule.traceForm_eq_sum_finrank_nsmul_mul, BilinForm.neg_right, RootPairing.RootPositiveForm.zero_lt_apply_root_root_iff, BilinForm.IsNonneg.smul, BilinForm.linMulLin_apply, BilinForm.comp_symmCompOfNondegenerate_apply, LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot, BilinForm.congr_fun, RootPairing.EmbeddedG2.twoShortAddLongRoot_shortRoot, BilinForm.IsAlt.sub, BilinForm.toMatrix'_toBilin', RootPairing.four_smul_rootForm_sq_eq_coxeterWeight_smul, Matrix.separatingLeft_toBilin_iff, BilinForm.isOrtho_def, BilinForm.Nondegenerate.toMatrix', LieModule.traceForm_apply_eq_zero_of_mem_lcs_of_mem_center, Matrix.SeparatingRight.toBilin', BilinForm.apply_eq_dotProduct_toMatrix_mulVec, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, BilinForm.toMatrix_compLeft, BilinForm.toMatrix_comp, BilinForm.IsAlt.add, LieModule.traceForm_apply_lie_apply', RootPairing.RootPositiveForm.algebraMap_posForm, BilinForm.SeparatingRight.toMatrix', BilinForm.Nondegenerate.toMatrix, BilinForm.congr_symm, BilinForm.baseChange_tmul, BilinForm.isSymm_iff_basis, Algebra.traceForm_toMatrix_powerBasis, BilinForm.nondegenerate_toBilin'_of_det_ne_zero', BilinForm.sum_apply, RootPairing.InvariantForm.apply_eq_or_of_apply_ne, RootPairing.InvariantForm.two_mul_apply_root_root, BilinForm.separatingLeft_toMatrix_iff, Matrix.toBilin'_toMatrix', BilinForm.IsAlt.smul, RootPairing.EmbeddedG2.threeShortAddLongRoot_longRoot, BilinForm.toMatrix'_compRight, Matrix.SeparatingRight.toBilin, Submodule.mem_traceDual_iff_isIntegral, RootPairing.polarization_apply_eq_zero_iff, RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_longRoot, Matrix.toBilin_comp, CliffordAlgebra.changeForm_changeForm, BilinForm.apply_smul_sub_smul_sub_eq, BilinForm.add_apply, BilinForm.sub_right, BilinForm.iIsOrtho_def, BilinForm.apply_dualBasis_right, Matrix.toBilin'_single, Module.Basis.traceDual_eq_iff, LieAlgebra.killingForm_of_equiv_apply
BilinMap 📖	CompOp	55 math math: LinearEquiv.congrRight₂_refl, QuadraticMap.smul_toBilin, QuadraticMap.canLift, BilinMap.polar_toQuadraticMap, LinearEquiv.congrRight_symm, BilinMap.toQuadraticMap_add, BilinMap.toQuadraticMapAddMonoidHom_apply, LinearEquiv.congrRight₂_apply, BilinMap.toQuadraticMap_zero, QuadraticMap.toBilinHom_apply, QuadraticMap.associated_eq_self_apply, QuadraticMap.associated_rightInverse, QuadraticMap.add_toBilin, QuadraticMap.associated_prod, QuadraticForm.polarBilin_tmul, QuadraticMap.associated_apply, QuadraticMap.polarBilin_injective, QuadraticMap.toQuadraticMap_associated, QuadraticMap.toBilin_apply, QuadraticMap.associated_tmul, QuadraticMap.choose_exists_companion, QuadraticMap.associated_toQuadraticMap, QuadraticMap.two_nsmul_associated, BilinMap.baseChange_tmul, QuadraticMap.associated_left_inverse', BilinMap.isSymm_iff_eq_flip, BilinMap.toQuadraticMap_smul, BilinMap.toQuadraticMapLinearMap_apply, BilinMap.toQuadraticMap_surjective, BilinMap.toQuadraticMap_list_sum, QuadraticForm.toDualProd_apply, QuadraticMap.canLift', BilinMap.toQuadraticMap_multiset_sum, BilinMap.tensorDistrib_tmul, QuadraticMap.coe_associatedHom, QuadraticMap.associated_linMulLin, QuadraticForm.associated_isSymm, QuadraticMap.exists_companion', BilinMap.toQuadraticMap_sum, LinearEquiv.congrRight₂_trans, QuadraticMap.associated_sq, QuadraticMap.associated_comp, QuadraticMap.associated_isOrtho, QuadraticMap.Ring.associated_pi, CliffordAlgebra.changeForm.associated_neg_proof, QuadraticMap.separatingLeft_of_anisotropic, BilinMap.toQuadraticMap_apply, BilinMap.polarBilin_toQuadraticMap, QuadraticMap.exists_companion, QuadraticForm.associated_tmul, QuadraticMap.associated_flip, QuadraticMap.associated_isSymm, BilinMap.toQuadraticMap_neg, QuadraticForm.associated_baseChange, BilinMap.toQuadraticMap_sub
compl₁₂ 📖	CompOp	26 math math: IsPerfPair.restrict, Matrix.toLinearMap₂'_comp, skewAdjointLieSubalgebraEquiv_apply, QuadraticMap.polarBilin_prod, skewAdjointLieSubalgebraEquiv_symm_apply, toMatrix₂'_compl₁₂, QuadraticMap.associated_prod, QuadraticMap.Ring.polarBilin_pi, Matrix.toLinearMap₂_compl₁₂, compl₁₂_inj, IsPerfPair.compl₁₂, toMatrix₂_compl₁₂, isPairSelfAdjoint_equiv, compl₁₂_id_id, mul_toMatrix₂_mul, compl₁₂_apply, QuadraticMap.associated_linMulLin, mul_toMatrix₂'_mul, trace_tensorProduct, QuadraticMap.associated_comp, QuadraticMap.Ring.associated_pi, Submodule.map₂_map_map, Bialgebra.mul_compr₂_comul, QuadraticMap.polarBilin_comp, Bialgebra.mul_compr₂_counit, BilinMap.toQuadraticMap_comp_same
compl₂ 📖	CompOp	13 math math: isAdjointPair_iff_comp_eq_compl₂, toMatrix₂_mul, compl₂_apply, toMatrix₂_compl₂, Submodule.map₂_map_right, TensorProduct.lift_comp_map, map_mul_iff, CliffordAlgebra.forall_mul_self_eq_iff, toMatrix₂'_mul, Module.End.lTensorAlgHom_apply_apply, toMatrix₂'_compl₂, rid_comp_lTensor, compl₂_id
compr₂ 📖	CompOp	22 math math: TensorPower.gMul_eq_coe_linearMap, LinearEquiv.congrRight₂_apply, injective_compr₂_of_injective, bijective_compr₂_of_equiv, CliffordAlgebra.EvenHom.compr₂_bilin, compr₂_apply, surjective_compr₂_of_equiv, map_mul_iff, Submodule.map_map₂, CliffordAlgebra.forall_mul_self_eq_iff, CliffordAlgebra.even.lift_symm_apply_bilin, Rep.coinvariantsTensor_hom_ext_iff, surjective_compr₂_of_exists_rightInverse, trace_tensorProduct, ModuleCat.ofHom₂_compr₂, compQuadraticMap_polarBilin, TensorProduct.lift_compr₂, trace_comp_comm, Bialgebra.mul_compr₂_comul, LieAlgebra.Extension.twoCocycleOf_coe_coe, TensorProduct.lift_mk_compr₂, Bialgebra.mul_compr₂_counit
compr₂ₛₗ 📖	CompOp	8 math math: surjective_compr₂ₛₗ_of_exists_rightInverse, injective_compr₂ₛₗ_of_injective, TensorProduct.lift_compr₂ₛₗ, surjective_compr₂ₛₗ_of_equiv, bijective_compr₂ₛₗ_of_equiv, TensorProduct.lift_mk_compr₂ₛₗ, TensorProduct.ext_iff, compr₂ₛₗ_apply
domRestrict₁₂ 📖	CompOp	6 math math: IsRefl.domRestrict, IsSymm.domRestrict, BilinForm.nondegenerate_restrict_iff_disjoint_ker, IsSymm.nondegenerate_restrict_of_isCompl_ker, nondegenerate_restrict_of_disjoint_orthogonal, domRestrict₁₂_apply
domRestrict₂ 📖	CompOp	1 math math: domRestrict₂_apply
flip 📖	CompOp	98 math math: subset_bipolar, Rep.MonoidalClosed.linearHomEquiv_symm_hom, LinearEquiv.coe_toLinearMap_flip, TensorProduct.sum_tmul_basis_right_injective, IsRefl.ker_flip_eq_bot, rTensor_comp_flip_mk, PointedCone.subset_dual_dual, isSymm_iff_eq_flip, RootPairing.injOn_dualMap_subtype_span_root_coroot, TensorProduct.flip_mk_surjective, Rep.homEquiv_apply_hom, flip_injective_iff₁, IsRefl.ker_eq_bot_iff_ker_flip_eq_bot, Rep.ihom_ev_app_hom, ProperCone.subset_dual_dual, flip_surjective_iff₁, isAlt_iff_eq_neg_flip, RootPairing.corootSpan_map_flip_toPerfPair, IsPerfectCompl.isCompl_right, IsPerfectCompl.flip_iff, lsmul_flip_apply, Submodule.dualCoannihilator_map_linearEquiv_flip, flip_bijective_iff₁, flip_bijective_iff₂, separatingRight_iff_flip_ker_eq_bot, flip.instIsPerfPair, Subspace.flip_quotDualCoannihilatorToDual_bijective, flip_apply, BilinMap.isSymm_iff_eq_flip, VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, flip_mul, RootPairing.toPerfPair_flip_comp_coroot, Submodule.map₂_span_singleton_eq_map_flip, apply_toPerfPair_flip, polar_gc, polar_weak_closed, RootPairing.coroot_root_two, flip_separatingRight, flip_injective_iff₂, RootPairing.reflection_dualMap_eq_coreflection, IsRefl.flip_isRefl_iff, isOrtho_flip, QuadraticMap.canLift', ProperCone.dual_flip_dual, ModuleCat.ihom_coev_app, Submodule.map₂_flip, IsPerfPair.bijective_right, IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap, tripolar_eq_polar, CliffordAlgebra.forall_mul_self_eq_iff, RootPairing.coroot_root_eq_pairing, separatingDual_iff_injective, IsContPerfPair.bijective_right, ProperCone.dual_dual_flip, flip_innerₗ, flip_nondegenerate, VectorFourier.integral_bilin_fourierIntegral_eq_flip, Rep.MonoidalClosed.linearHomEquiv_hom, isSymmetric_iff_sesqForm, Rep.homEquiv_symm_apply_hom, polar_isClosed, RootPairing.flip_toLinearMap, Representation.leftRegular_norm_apply, RootPairing.toPerfPair_flip_conj_coreflection, TensorProduct.equivFinsuppOfBasisRight_symm, Rep.ihom_coev_app_hom, rid_comp_lTensor, Coalgebra.lTensor_counit_comp_comul, ContinuousLinearMap.isAdjointPair_inner, flip_separatingLeft, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, VectorFourier.integral_fourierIntegral_smul_eq_flip, trace_comp_comm, TensorProduct.lift_comp_comm_eq, BilinMap.polarBilin_toQuadraticMap, Algebra.FormallyUnramified.comp_sec, Real.zero_at_infty_vector_fourierIntegral, LieModule.traceForm_flip, PointedCone.dual_flip_dual_dual_flip, flip_surjective_iff₂, Submodule.map_dualCoannihilator_linearEquiv_flip, TensorProduct.toLinearMap_symm_rid, flip_flip, dualCoannihilator_range_eq_ker_flip, QuadraticMap.associated_flip, isOrthoᵢ_flip, isAdjointPair_inner, IsPerfectCompl.flip, le_comap_range_rTensor, IsPerfPair.flip, ModuleCat.ihom_ev_app, PointedCone.dual_dual_flip_dual, Submodule.flip_quotDualCoannihilatorToDual_injective, lflip_apply, IsRefl.ker_flip, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, flip.instIsContPerfPair, dualAnnihilator_ker_eq_range_flip
lcomp 📖	CompOp	9 math math: rTensor_injective_iff_lcomp_surjective, lcomp_injective_of_surjective, lcomp_apply, lcomp_apply', CharacterModule.dual_rTensor_conj_homEquiv, dualMap_eq_lcomp, exact_lcomp_of_exact_of_surjective, ModuleCat.monoidalClosed_pre_app, ModuleCat.ihom_ev_app
lcompₛₗ 📖	CompOp	1 math math: lcompₛₗ_apply
lflip 📖	CompOp	2 math math: lflip_symm, lflip_apply
llcomp 📖	CompOp	4 math math: llcomp_apply, llcomp_apply', Rep.ihom_map_hom, trace_comp_comm
lsmul 📖	CompOp	24 math math: Submodule.smul_eq_map₂, ModN.basis_apply_eq_mkQ, lsmul_flip_apply, lsmul_injective, lsmul_eq_DistribMulAction_toLinearMap, Module.isTorsionBySet_iff_subseteq_ker_lsmul, lsmul_apply, Coalgebra.lift_lsmul_comp_counit_comp_comul, Module.isTorsionBy_iff_mem_ker_lsmul, lift_lsmul_mul_eq_lsmul_lift_lsmul, IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap, Module.Flat.iff_lift_lsmul_comp_subtype_injective, trace_tensorProduct, Representation.leftRegular_norm_apply, rid_comp_lTensor, isSMulRegular_on_quot_iff_lsmul_comap_eq, Algebra.injective_lift_lsmul, lid_comp_rTensor, isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule, isSMulRegular_iff_ker_lsmul_eq_bot, ModN.instModuleFinite, ker_lsmul, isSMulRegular_on_quot_iff_lsmul_comap_le, lsmul_eq_distribSMultoLinearMap
mk₂ 📖	CompOp	1 math math: mk₂_apply
mk₂' 📖	CompOp	1 math math: mk₂'_apply
mk₂'ₛₗ 📖	CompOp	1 math math: mk₂'ₛₗ_apply
restrictScalarsRange 📖	CompOp	3 math math: eq_restrictScalarsRange_iff, restrictScalarsRange_apply, restrictScalarsRange_apply_eq_zero_iff
restrictScalarsRange₂ 📖	CompOp	6 math math: restrictScalarsRange₂_apply, IsPerfPair.restrictScalars, restrictScalarsRange₂_apply_eq_zero_iff, restrictScalarsField_apply_apply, eq_restrictScalarsRange₂_iff, IsPerfPair.restrictScalars_of_field
restrictScalars₁₂ 📖	CompOp	4 math math: restrictScalars₁₂_inj, restrictScalars₁₂_injective, restrictScalars₁₂_apply_apply, Algebra.injective_lift_lsmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_compr₂_of_equiv 📖	mathematical	Function.Bijective LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike	compr₂ Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearEquiv.toLinearMap RingHomInvPair.ids	—	smulCommClass_self RingHomInvPair.ids IsScalarTower.left injective_compr₂_of_injective LinearEquiv.bijective surjective_compr₂_of_equiv
bijective_compr₂ₛₗ_of_equiv 📖	mathematical	Function.Bijective LinearMap CommSemiring.toSemiring DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike	compr₂ₛₗ LinearEquiv.toLinearMap	—	smulCommClass_self injective_compr₂ₛₗ_of_injective LinearEquiv.bijective surjective_compr₂ₛₗ_of_equiv
compl₁₂_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike addCommMonoid module compl₁₂	—	—
compl₁₂_id_id 📖	mathematical	—	compl₁₂ id	—	ext
compl₁₂_inj 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	compl₁₂	—	ext congr_fun₂
compl₂_apply 📖	mathematical	—	DFunLike.coe LinearMap instFunLike addCommMonoid module compl₂	—	—
compl₂_id 📖	mathematical	—	compl₂ RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids id	—	ext RingHomCompTriple.ids compl₂_apply id_coe
compr₂_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike addCommMonoid module compr₂	—	—
compr₂ₛₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring instFunLike addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction compr₂ₛₗ	—	smulCommClass_self
congr_fun₂ 📖	mathematical	—	DFunLike.coe LinearMap instFunLike addCommMonoid module	—	congr_fun
domRestrict₁₂_apply 📖	mathematical	—	DFunLike.coe LinearMap Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module instFunLike addCommMonoid module domRestrict₁₂	—	—
domRestrict₂_apply 📖	mathematical	—	DFunLike.coe LinearMap Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module instFunLike addCommMonoid module domRestrict₂	—	—
eq_restrictScalarsRange_iff 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike Submodule SetLike.instMembership Submodule.setLike range RingHomSurjective.ids	restrictScalarsRange	—	RingHomSurjective.ids restrictScalarsRange_apply
eq_restrictScalarsRange₂_iff 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike Submodule SetLike.instMembership Submodule.setLike range RingHomSurjective.ids addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	restrictScalarsRange₂	—	smulCommClass_self RingHomSurjective.ids restrictScalarsRange₂_apply
ext_iff₂ 📖	mathematical	—	DFunLike.coe LinearMap instFunLike addCommMonoid module	—	congr_fun₂ ext₂
ext₂ 📖	—	DFunLike.coe LinearMap instFunLike addCommMonoid module	—	—	ext
flip_apply 📖	mathematical	—	DFunLike.coe LinearMap instFunLike addCommMonoid module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction flip	—	SMulCommClass.symm
flip_flip 📖	mathematical	—	flip SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	ext₂ SMulCommClass.symm flip_apply
flip_inj 📖	—	flip	—	—	SMulCommClass.symm ext₂
injective_compr₂_of_injective 📖	mathematical	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike	compr₂ Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	smulCommClass_self RingHomCompTriple.ids Function.Injective.injective_linearMapComp_left
injective_compr₂ₛₗ_of_injective 📖	mathematical	LinearMap CommSemiring.toSemiring DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike	compr₂ₛₗ	—	smulCommClass_self Function.Injective.injective_linearMapComp_left
ker_lsmul 📖	mathematical	—	ker CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike lsmul Bot.bot Submodule Submodule.instBot	—	ker_eq_bot_of_injective smulCommClass_self lsmul_injective
lcomp_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike addCommMonoid module lcomp	—	—
lcomp_apply' 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid module instFunLike lcomp comp RingHomCompTriple.ids	—	—
lcomp_injective_of_surjective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	addCommMonoid module lcomp	—	Function.Surjective.injective_linearMapComp_right RingHomCompTriple.ids
lcompₛₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap instFunLike RingHom.id Semiring.toNonAssocSemiring addCommMonoid module lcompₛₗ	—	—
lflip_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap addCommMonoid module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike lflip flip	—	SMulCommClass.symm RingHomInvPair.ids instSMulCommClass
lflip_symm 📖	mathematical	—	LinearEquiv.symm LinearMap addCommMonoid module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSMulCommClass RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids lflip	—	RingHomInvPair.ids SMulCommClass.symm instSMulCommClass
llcomp_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring instFunLike addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id Semiring.toNonAssocSemiring instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero llcomp	—	smulCommClass_self instSMulCommClass
llcomp_apply' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike RingHom.id Semiring.toNonAssocSemiring instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero llcomp comp	—	smulCommClass_self instSMulCommClass
lsmul_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction lsmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	smulCommClass_self
lsmul_eq_DistribMulAction_toLinearMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike lsmul DistribSMul.toLinearMap DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	lsmul_eq_distribSMultoLinearMap
lsmul_eq_distribSMultoLinearMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike lsmul DistribSMul.toLinearMap DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	smulCommClass_self
lsmul_injective 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction lsmul	—	smul_right_injective IsDomain.toIsCancelMulZero
map_add₂ 📖	mathematical	—	DFunLike.coe LinearMap instFunLike addCommMonoid module AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	map_add SMulCommClass.symm
map_neg₂ 📖	mathematical	—	DFunLike.coe LinearMap AddCommGroup.toAddCommMonoid instFunLike addCommMonoid module NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_neg SMulCommClass.symm
map_smul₂ 📖	mathematical	—	DFunLike.coe LinearMap instFunLike RingHom.id Semiring.toNonAssocSemiring addCommMonoid module SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	map_smul SMulCommClass.symm
map_smulₛₗ₂ 📖	mathematical	—	DFunLike.coe LinearMap instFunLike addCommMonoid module SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	map_smulₛₗ SMulCommClass.symm
map_sub₂ 📖	mathematical	—	DFunLike.coe LinearMap AddCommGroup.toAddCommMonoid instFunLike addCommMonoid module SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	map_sub SMulCommClass.symm
map_sum₂ 📖	mathematical	—	DFunLike.coe LinearMap instFunLike addCommMonoid module Finset.sum	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass SMulCommClass.symm
map_zero₂ 📖	mathematical	—	DFunLike.coe LinearMap instFunLike addCommMonoid module AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_zero SMulCommClass.symm
mk₂'_apply 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike addCommMonoid module mk₂'	—	—
mk₂'ₛₗ_apply 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	LinearMap instFunLike addCommMonoid module mk₂'ₛₗ	—	—
mk₂_apply 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid mk₂	—	smulCommClass_self
restrictScalarsRange_apply 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike Submodule SetLike.instMembership Submodule.setLike range RingHomSurjective.ids	restrictScalarsRange	—	RingHomSurjective.ids RingHomCompTriple.ids IsScalarTower.compatibleSMul RingHomCompTriple.right_ids comp_codLift comp_apply restrictScalars_apply
restrictScalarsRange_apply_eq_zero_iff 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike Submodule SetLike.instMembership Submodule.setLike range RingHomSurjective.ids	restrictScalarsRange AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomSurjective.ids restrictScalarsRange_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass
restrictScalarsRange₂_apply 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike Submodule SetLike.instMembership Submodule.setLike range RingHomSurjective.ids addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	restrictScalarsRange₂	—	smulCommClass_self RingHomSurjective.ids codRestrict₂_apply
restrictScalarsRange₂_apply_eq_zero_iff 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike Submodule SetLike.instMembership Submodule.setLike range RingHomSurjective.ids addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	restrictScalarsRange₂ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	smulCommClass_self RingHomSurjective.ids restrictScalarsRange₂_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass
restrictScalars₁₂_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike addCommMonoid module restrictScalars₁₂	—	—
restrictScalars₁₂_inj 📖	mathematical	—	restrictScalars₁₂	—	restrictScalars₁₂_injective
restrictScalars₁₂_injective 📖	mathematical	—	LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid module restrictScalars₁₂	—	ext₂ congr_fun₂
surjective_compr₂_of_equiv 📖	mathematical	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike	compr₂ Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearEquiv.toLinearMap RingHomInvPair.ids	—	smulCommClass_self RingHomInvPair.ids surjective_compr₂_of_exists_rightInverse RingHomCompTriple.ids LinearEquiv.symm_trans_self
surjective_compr₂_of_exists_rightInverse 📖	mathematical	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike comp RingHomCompTriple.ids id	compr₂ Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	smulCommClass_self RingHomCompTriple.ids surjective_comp_left_of_exists_rightInverse RingHomInvPair.ids
surjective_compr₂ₛₗ_of_equiv 📖	mathematical	LinearMap CommSemiring.toSemiring DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike	compr₂ₛₗ LinearEquiv.toLinearMap	—	smulCommClass_self surjective_compr₂ₛₗ_of_exists_rightInverse RingHomInvPair.triples₂ RingHomInvPair.ids LinearEquiv.symm_trans_self
surjective_compr₂ₛₗ_of_exists_rightInverse 📖	mathematical	LinearMap CommSemiring.toSemiring DFunLike.coe addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ id	compr₂ₛₗ	—	smulCommClass_self RingHomInvPair.triples₂ surjective_comp_left_of_exists_rightInverse

---

← Back to Index