DFinsupp

📁 Source: Mathlib/LinearAlgebra/DFinsupp.lean

Statistics

Metric	Count
Definitions coprodMap, domLCongr, instEquivLikeLinearEquiv, lapply, linearEquivFunOnFintype, lmk, lsingle, lsum, linearEquiv, linearMap, sigmaCurryLEquiv, linearEquiv	12
Theorems coprodMap_apply, coprodMap_apply_single, domLCongr_apply, iSup_range_lsingle, injective_pi_lapply, ker_mapRangeAddMonoidHom, ker_mapRangeLinearMap, lapply_apply, lapply_comp_lsingle_of_ne, lapply_comp_lsingle_same, lhom_ext, lhom_ext', lhom_ext'_iff, linearEquivFunOnFintype_apply, linearEquivFunOnFintype_symm_apply, lmk_apply, lsingle_apply, lsum_apply_apply, lsum_lsingle, lsum_single, lsum_symm_apply, linearEquiv_apply, linearEquiv_refl, linearEquiv_symm, linearEquiv_trans, linearMap_apply, linearMap_comp, linearMap_id, mapRange_smul, mker_mapRangeAddMonoidHom, mrange_mapRangeAddMonoidHom, range_mapRangeAddMonoidHom, range_mapRangeLinearMap, sigmaCurryLEquiv_apply, sigmaCurryLEquiv_symm_apply, linearMap, map_dfinsuppSumAddHom, coe_dfinsuppSum, dfinsuppSum_apply, map_dfinsuppSumAddHom, biSup_eq_range_dfinsupp_lsum, dfinsuppSumAddHom_mem, dfinsuppSum_mem, iSup_eq_range_dfinsupp_lsum, mem_biSup_iff_exists_dfinsupp, mem_iSup_finset_iff_exists_sum, mem_iSup_iff_exists_dfinsupp, mem_iSup_iff_exists_dfinsupp', mem_iSup_iff_exists_finsupp, dfinsuppSumAddHom_injective, dfinsupp_lsum_injective, linearEquiv_apply, linearEquiv_symm_apply, linearIndependent, iSupIndep_iff_dfinsuppSumAddHom_injective, iSupIndep_iff_dfinsupp_lsum_injective, iSupIndep_iff_finset_sum_eq_imp_eq, iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero, iSupIndep_iff_forall_dfinsupp, iSupIndep_iff_linearIndependent_of_ne_zero, iSupIndep_of_dfinsuppSumAddHom_injective, iSupIndep_of_dfinsuppSumAddHom_injective', iSupIndep_of_dfinsupp_lsum_injective, lsum_comp_mapRange_toSpanSingleton	64
Total	76

DFinsupp

Definitions

Name	Category	Theorems
coprodMap 📖	CompOp	2 math math: coprodMap_apply, coprodMap_apply_single
domLCongr 📖	CompOp	2 math math: MultilinearMap.freeDFinsuppEquiv_def, domLCongr_apply
instEquivLikeLinearEquiv 📖	CompOp	1107 math math: Pi.comul_eq_adjoint, LinearMap.det_toContinuousLinearMap, DirectSum.IsInternal.ofBijective_coeLinearMap_same, TensorProduct.finsuppRight_apply, LinearMap.lTensor_ker_subtype_tensorKerEquiv_symm, RootPairing.InvariantForm.apply_reflection_reflection, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr, LinearMap.restrictScalars_toMatrix, LinearMap.apply_symm_toPerfPair_self, LinearMap.SeparatingRight.toMatrix₂', Submodule.rTensorOne_symm_apply, iSupIndep.linearEquiv_symm_apply, TensorProduct.enorm_lid, LinearMap.charpoly_def, iSupIndep.dfinsupp_lsum_injective, lsum_lsingle, Matrix.toLin_kronecker, QuaternionAlgebra.coe_linearEquivTuple_symm, Matrix.SeparatingLeft.toBilin', LinearMap.detAux_def'', TensorProduct.LieModule.liftLie_apply, Matrix.kroneckerTMulStarAlgEquiv_symm_apply, LinearMap.BilinForm.toMatrix_toBilin, Algebra.Presentation.differentials.comm₁₂_single, LinearMap.adjoint_adjoint, Matrix.SeparatingRight.toLinearMap₂, Rep.MonoidalClosed.linearHomEquiv_symm_hom, MultilinearMap.fromDFinsuppEquiv_apply, LinearEquiv.flip_apply, SimpleGraph.lapMatrix_toLinearMap₂', RootPairing.coroot_eq_polarizationEquiv_apply_root, MvPolynomial.rTensor_apply_tmul_apply, Matrix.separatingRight_toLinearMap₂'_iff, QuadraticMap.sum_polar_sub_repr_sq, MvPolynomial.scalarRTensor_apply_monomial_tmul, Polynomial.toMatrix_sylvesterMap', Module.basisUnique_repr_eq_zero_iff, Matrix.toLinearMapRight'_mul, finsuppTensorFinsupp_apply, TensorPower.cast_cast, LinearMap.isPositive_adjoint_comp_self, Matrix.separatingRight_toLinearMap₂_iff, NumberField.Units.fun_eq_repr, Matrix.spectrum_toEuclideanLin, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, KaehlerDifferential.polynomialEquiv_symm, TensorProduct.equivFinsuppOfBasisLeft_symm_apply, Submodule.tensorEquivSpan_apply_tmul, IsBaseChange.basis_repr_comp_apply, MeasureTheory.Measure.MapLinearEquiv.isAddHaarMeasure, PiTensorProduct.ofDirectSumEquiv_tprod_lof, RootPairing.two_nsmul_reflection_eq_of_perm_eq, LinearMap.BilinForm.toMatrixAux_eq, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', IsAdjoinRootMonic.coeff_apply, Matrix.toLinearMap₂'_comp, kroneckerTMulAlgEquiv_symm_single_tmul, Representation.finsupp_apply, LinearMap.toMatrix_apply', LinearMap.toMatrix₂_mul, ZMod.LFunction_one_sub, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, Matrix.repr_toLin, KaehlerDifferential.mvPolynomialBasis_repr_D_X, TensorProduct.sum_tmul_basis_right_injective, ZMod.dft_even_iff, ZMod.invDFT_apply, RootPairing.Equiv.coweightEquiv_symm_coweightMap, RootPairing.coreflection_image_eq, LinearMap.BilinForm.toMatrix_compRight, TensorProduct.enorm_comm, LinearMap.adjoint_innerₛₗ_apply, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, Submodule.dualQuotEquivDualAnnihilator_apply, WittVector.IsocrystalHom.frob_equivariant, LinearMap.adjoint_eq_toCLM_adjoint, exteriorPower.basis_repr_ne, TensorProduct.gradedComm_tmul_one, PolynomialModule.aeval_equivPolynomial, Matrix.toLinearMap₂_toMatrix₂, LinearMap.toMatrix_one, LinearMap.isSelfAdjoint_toContinuousLinearMap_iff, Rep.diagonalHomEquiv_symm_apply, Matrix.separatingRight_toBilin_iff, IsBaseChange.of_fintype_basis_eq, Matrix.spectrum_toLpLin, Coalgebra.coassoc_symm_apply, Matrix.toLin_mul_apply, LinearMap.tensorEqLocusEquiv_apply, toMatrix_distrib_mul_action_toLinearMap, LinearMap.BilinForm.toMatrix'_apply, LinearMap.BilinForm.SeparatingRight.toMatrix, LinearMap.nondegenerate_toLinearMap₂'_of_det_ne_zero', MvPolynomial.scalarRTensor_apply_X_tmul_apply, ZMod.dft_mul_const, Matrix.Nondegenerate.toLinearMap₂, Matrix.kroneckerTMul_assoc', Module.AEval.of_symm_smul, Matrix.intrinsicStar_toLin', Module.Basis.ofZLatticeComap_apply, LinearMap.coe_toContinuousLinearMap', KaehlerDifferential.polynomialEquiv_D, continuous_equivFun_basis, QuadraticMap.toMatrix'_comp, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, exteriorPower.alternatingMapLinearEquiv_ιMulti, TensorProduct.directSum_lof_tmul_lof, DirectSum.lequivCongrLeft_apply, star_dotProduct_toMatrix₂_mulVec, IsLocalFrameOn.coeff_apply_of_mem, LinearMap.spectrum_toMatrix', Real.smul_map_diagonal_volume_pi, toMatrix_rotation, LieModule.shiftedGenWeightSpace.toEnd_eq, IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, QuotSMulTop.equivTensorQuot_naturality_mk, NormedSpace.Dual.toWeakDual_continuous, Matrix.toLpLin_mul_same, TensorProduct.coe_directSumRight', finsuppTensorFinsupp'_symm_single_eq_tmul_single_one, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, QuadraticAlgebra.linearEquivTuple_apply, LinearMap.toMatrix_baseChange, RootPairing.toPerfPair_comp_root, TensorProduct.adjoint_map, LinearIsometryEquiv.lTensor_apply, LinearMap.trace_eq_matrix_trace_of_finset, LinearMap.adjoint_toContinuousLinearMap, Matrix.SeparatingLeft.toLinearMap₂', TensorProduct.dualDistrib_apply_comm, LieHom.quotKerEquivRange_toFun, RootPairing.mapsTo_reflection_root, LinearMap.BilinForm.nondegenerate_toMatrix_iff, LinearMap.rank_diagonal, TensorProduct.directLimitRight_tmul_of, LinearMap.separatingRight_toMatrix₂'_iff, Matrix.toEuclideanLin_apply, Submodule.biSup_eq_range_dfinsupp_lsum, Algebra.toMatrix_lmul_eq, isAdjointPair_toLinearMap₂, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply, exteriorPower.alternatingMapLinearEquiv_symm_map, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, Module.AEval'.X_smul_of, Finsupp.basis_repr, Matrix.toBilin_apply, IsLocalRing.basisQuotient_repr, LinearMap.toMatrix₂'_compl₁₂, Representation.smul_ofModule_asModule, Module.Basis.toLin_toMatrix, Matrix.toLinearEquivRight'OfInv_symm_apply, Pi.counit_eq_adjoint, Matrix.toLin'_mul_apply, MultilinearMap.fromDirectSumEquiv_symm_apply, Matrix.toLinearMapₛₗ₂'_single, Matrix.nondegenerate_toBilin'_iff, Representation.coinvariantsFinsuppLEquiv_apply, LinearMap.toMatrixAlgEquiv_apply, GradedTensorProduct.auxEquiv_one, Algebra.TensorProduct.basis_repr_tmul, RootPairing.reflection_apply_root', LinearMap.toMatrix'_toLin', TensorProduct.toMatrix_assoc, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, Matrix.toLinearMap₂'_apply', SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, LinearMap.toMatrix_id, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, RootPairing.IsOrthogonal.reflection_apply_left, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, PositiveLinearMap.preGNS_norm_def, LinearMap.eq_adjoint_iff_basis_left, Matrix.mul_reindexLinearEquiv_one, TensorPower.algebraMap₀_mul, TensorProduct.gradedComm_algebraMap_tmul, IsAdjoinRootMonic.basis_repr, LinearMap.toMatrix_transpose, WeakDual.toStrongDual_inj, LinearMap.toMatrix₂_toLinearMapₛₗ₂, TensorProduct.finsuppLeft_smul', Algebra.TensorProduct.basisAux_map_smul, Pi.basis_repr_single, LinearIsometryEquiv.coe_toLinearEquiv, TensorProduct.equivFinsuppOfBasisRight_apply_tmul, Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap, Module.Basis.sumQuot_repr_left, Coalgebra.comm_comul, Module.reflection_apply_self, Polynomial.degreeLT.addLinearEquiv_castAdd, KaehlerDifferential.polynomialEquiv_comp_D, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LinearEquiv.toSpanNonzeroSingleton_homothety, IsBaseChange.endHom_toMatrix, LocalizedModule.equivTensorProduct_apply_mk, Real.map_matrix_volume_pi_eq_smul_volume_pi, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul, Module.Basis.toMatrix_map, PiTensorProduct.ofFinsuppEquiv'_tprod_single, TensorProduct.lidIsometry_apply, StrongDual.toWeakDual_inj, LinearMap.BilinForm.Nondegenerate.congr, Rep.MonoidalClosed.linearHomEquivComm_hom, LinearMap.tensorKerEquivOfSurjective_symm_tmul, TensorProduct.equivFinsuppOfBasisLeft_symm, Module.Basis.coe_toOrthonormalBasis_repr, RootPairing.IsOrthogonal.coreflection_apply_right, Matrix.toLinearMap₂'_apply, WeakDual.coe_toStrongDual, Polynomial.degreeLT.addLinearEquiv_apply_fst, lTensorHomEquivHomLTensor_apply, LinearMap.BilinForm.separatingLeft_toMatrix'_iff, TensorProduct.finsuppScalarRight_apply, RootPairing.reflection_same, LocalizedModule.equivTensorProduct_symm_apply_tmul, TensorProduct.finsuppScalarRight_apply_tmul, Representation.single_smul, ContinuousLinearMap.toUniformConvergenceCLM_apply, Module.FinitePresentation.linearEquivMap_symm_apply, Matrix.isNilpotent_toLin'_iff, Orientation.volumeForm_zero_pos, Module.Basis.constrL_apply, Module.AEval'.of_symm_X_smul, homTensorHomEquiv_apply, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, Matrix.toLinearEquiv'_symm_apply, LinearMap.BilinForm.mul_toMatrix'_mul, Trivialization.linearEquivAt_apply, finsuppTensorFinsupp'_single_tmul_single, NumberField.canonicalEmbedding.integralBasis_repr_apply, BilinForm.mul_toMatrix_mul, QuadraticForm.tensorRId_symm_apply, Module.Basis.linearMap_apply, CoalgEquiv.coe_toLinearEquiv, Matrix.toLinearMap₂_compl₁₂, PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod, Module.Invertible.linearEquivOfRightInverse_symm_apply, PiTensorProduct.ofFinsuppEquiv_tprod_single, LinearEquiv.coe_ofInjectiveEndo, LinearMap.isSymmetric_adjoint_mul_self, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, TensorPower.mul_assoc, RootPairing.Equiv.weightMap_weightEquiv_symm, Representation.coinvariantsTprodLeftRegularLEquiv_apply, ZMod.dft_comp_unitMul, LinearMap.toMatrix₂_compl₂, finsuppTensorFinsuppLid_symm_single_smul, Module.reflection_mul_reflection_pow_apply, sum_mapRange_index.linearMap, rTensorHomEquivHomRTensor_apply, TensorPower.algebraMap₀_one, dualTensorHomEquivOfBasis_symm_cancel_right, Matrix.toLpLin_symm_pow, MvPolynomial.scalarRTensor_apply_tmul, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', finsuppTensorFinsupp'_symm_single_mul, LinearMap.polyCharpolyAux_map_eval, Matrix.toLinearMapₛₗ₂'_aux_eq, ZSpan.repr_ceil_apply, ZLattice.comap_equiv_apply, Matrix.linfty_opNNNorm_toMatrix, KaehlerDifferential.tensorKaehlerEquivBase_tmul, Module.Basis.coe_constrL, MulOpposite.isometry_opLinearEquiv, Algebra.traceForm_toMatrix, basis_toMatrix_basisFun_mul, Matrix.toLin_scalar, GradedTensorProduct.auxEquiv_symm_one, LinearMap.adjoint_rTensor, GradedTensorProduct.auxEquiv_comm, TensorProduct.finsuppLeft_symm_apply_single, LinearMap.adjoint_inner_right, BilinForm.dotProduct_toMatrix_mulVec, Module.invOn_reflection_of_mapsTo, Matrix.toLpLin_one, Convex.toWeakSpace_closure, finsuppTensorFinsupp'_apply_apply, PiTensorProduct.ofFinsuppEquiv_symm_single_tprod, LinearMap.isPosSemidef_iff_posSemidef_toMatrix, PositiveLinearMap.preGNS_inner_def, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, RootPairing.Equiv.weightEquiv_apply, Polynomial.degreeLT.addLinearEquiv_apply_snd, TensorProduct.inner_lid_lid, LinearMap.BilinForm.tensorDistribEquiv_apply, Matrix.piLp_ofLp_toEuclideanLin, LinearMap.BilinForm.toMatrix_apply, Module.Basis.sumQuot_repr_inl, TensorProduct.norm_comm, PowerBasis.constr_pow_algebraMap, lieEquivMatrix'_apply, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, BilinForm.toMatrix_toBilin, WeakDual.isCompact_closedBall, Matrix.toPerfectPairing_apply_apply, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, Module.DirectLimit.congr_symm_apply_of, Algebra.Generators.cotangentSpaceBasis_repr_tmul, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, LinearMap.minpoly_toMatrix', RootPairing.RootPositiveForm.isOrthogonal_reflection, LinearMap.toMatrix₂_comp, TensorProduct.gradedComm_algebraMap, Matrix.SeparatingRight.toLinearMap₂', Representation.asModuleEquiv_symm_map_smul, TensorProduct.norm_assoc, LinearEquiv.transvection.apply, WittVector.IsocrystalEquiv.frob_equivariant, Submodule.mem_iSup_iff_exists_dfinsupp, QuadraticForm.tensorRId_apply, MvPolynomial.rTensor_apply_X_tmul, PiLp.basisFun_repr, Matrix.toLpLin_pow, KaehlerDifferential.tensorKaehlerEquiv_tmul, Module.AEval'.X_pow_smul_of, Algebra.Generators.H1Cotangent.δAux_toAlgHom, RootPairing.InvariantForm.isOrthogonal_reflection, Matrix.kroneckerAlgEquiv_apply, InnerProductSpace.AlgebraOfCoalgebra.mul_def, LinearMap.BilinForm.separatingRight_toMatrix'_iff, Matrix.isUnit_toLin'_iff, Module.piEquiv_apply_apply, Matrix.toLin'_mul, Submodule.iSup_eq_range_dfinsupp_lsum, TensorProduct.gradedComm_tmul_of_zero, LinearMap.isNilpotent_toMatrix_iff, TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply, LinearMap.BilinForm.dotProduct_toMatrix_mulVec, LinearMap.det_eq_det_toMatrix_of_finset, LinearMap.toMatrix_reindexRange, LinearMap.IsReflective.reflective_reflection, Matrix.ofLp_toLpLin, TensorPower.galgebra_toFun_def, Module.range_piEquiv, LinearMap.toMatrix_smulBasis_left, Module.Basis.coe_toOrthonormalBasis_repr_symm, LinearMap.BilinForm.isSymm_iff_flip, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, MultilinearMap.fromDFinsuppEquiv_single, LinearMap.det_toLin', DirectSum.coe_congr_linearEquiv, Matrix.rank_eq_finrank_range_toLin, MvPolynomial.rTensor_apply_tmul, Matrix.toLinearMapRight'_mul_apply, BilinForm.toMatrix_comp, Matrix.reindexLinearEquiv_one, PiTensorProduct.norm_eval_le_injectiveSeminorm, FiniteDimensional.basisSingleton_repr_apply, Matrix.toLin_mul, Matrix.toLin_pow, Submodule.coe_tensorSpanEquivSpan_apply_tmul, Module.Basis.equivFunL_symm_apply_repr, Submodule.FG.lTensor.directLimit_apply', TensorProduct.directSumLeft_tmul_lof, PowerBasis.repr_gen_pow_isIntegral, Matrix.toLin_self, kroneckerTMulLinearEquiv_one, Module.DirectLimit.linearEquiv_of, Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, PositiveLinearMap.toPreGNS_ofPreGNS, Module.Basis.mulOpposite_repr_op, LinearMap.separatingLeft_toMatrix₂'_iff, hasEigenvector_toLin'_diagonal, Matrix.GeneralLinearGroup.toLin'_apply, Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin, Submodule.FG.rTensor.directLimit_apply, TensorProduct.directLimitLeft_rTensor_of, TensorProduct.finsuppScalarRight_smul, Matrix.reindexLinearEquiv_comp, Matrix.toLinearMapₛₗ₂'_toMatrix', LinearMap.toMatrix'_algebraMap, Rep.resIndAdjunction_homEquiv_symm_apply, finsuppTensorFinsupp_single, PiTensorProduct.liftEquiv_symm_apply, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, RootPairing.bijOn_reflection_root, LinearMap.IsReflective.isOrthogonal_reflection, BilinearForm.toMatrixAux_eq, RootPairing.rootForm_reflection_reflection_apply, Matrix.SeparatingLeft.toBilin, Matrix.charpoly_toLin, QuadraticForm.tmul_tensorAssoc_apply, Module.DirectLimit.congr_apply_of, LinearMap.toMatrix_mulVec_repr, LinearMap.toMatrix_innerₛₗ_apply, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne, AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_symm_of, TensorProduct.gradedComm_one, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, Matrix.toLin_apply_eq_zero_iff, Matrix.nondegenerate_toBilin_iff, LinearMap.range_toContinuousLinearMap, Polynomial.mkDerivationEquiv_symm_apply, Matrix.toLin'_reindex, LinearMap.BilinForm.toDual_def, Matrix.PosSemidef.toLinearMap₂'_zero_iff, LinearMap.BilinForm.toMatrix'_compLeft, Matrix.toLinearMapₛₗ₂_apply, MultilinearMap.freeDFinsuppEquiv_single, WeakDual.isSeqCompact_closedBall, LinearMap.BilinForm.dualBasis_repr_apply, PiTensorProduct.liftEquiv_apply, LinearMap.isSelfAdjoint_iff', Orientation.areaForm'_apply, DirectSum.linearEquivFunOnFintype_lof, Module.Basis.sumQuot_repr_inl_of_mem, Module.Basis.end_apply, TensorPower.algebraMap₀_eq_smul_one, Matrix.Nondegenerate.toBilin, TensorProduct.finsuppScalarRight_apply_tmul_apply, LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero, LinearMap.toMatrix'_apply, PiTensorProduct.ofDFinsuppEquiv_tprod_apply, QuadraticForm.tmul_tensorComm_apply, Matrix.toLpLin_toLp, apply_eq_dotProduct_toMatrix₂_mulVec, Polynomial.degreeLT.addLinearEquiv_apply, Module.reflection_reflection_iterate, kroneckerLinearEquiv_symm_kronecker, LinearMap.coe_toContinuousLinearMap, LinearEquiv.coe_toContinuousLinearEquiv', LinearMap.BilinForm.separatingRight_toMatrix_iff, MultilinearMap.freeDFinsuppEquiv_def, TensorProduct.finsuppLeft_apply, LinearMap.BilinForm.SeparatingLeft.toMatrix', finsuppTensorFinsuppRid_symm_single_smul, mapRange.linearEquiv_apply, ZMod.invDFT_def', Matrix.ker_toLin_eq_bot, Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff, GradedTensorProduct.auxEquiv_mul, QuadraticForm.tmul_tensorRId_apply, LinearMap.IsSymmetric.adjoint_eq, Module.FinitePresentation.linearEquivMap_apply, LinearIsometryEquiv.coe_symm_toLinearEquiv, Module.Invertible.linearEquivOfLeftInverse_symm_apply, ProperCone.dual_singleton, Module.involutive_reflection, Algebra.TensorProduct.basisAux_tmul, LinearEquiv.coe_toContinuousLinearEquiv_symm', Module.AEval.X_pow_smul_of, Module.infinite_range_reflection_reflection_iterate_iff, LinearMap.polyCharpolyAux_map_eq_charpoly, LinearMap.toContinuousLinearMap_eq_iff_eq_toLinearMap, linearMap_toMatrix_mul_basis_toMatrix, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Matrix.kroneckerTMulAlgEquiv_symm_apply, Polynomial.mkDerivationEquiv_apply, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, Rep.resIndAdjunction_homEquiv_apply, RootPairing.toPerfPair_flip_comp_coroot, LinearMap.toMatrix_transpose_apply, Pi.basis_repr, Matrix.kroneckerTMulStarAlgEquiv_apply, toMatrix_dualTensorHom, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, Algebra.Generators.H1Cotangent.δAux_ofComp, LinearMap.isPositive_toContinuousLinearMap_iff, Matrix.range_toLin', ZMod.dft_apply, LinearMap.mul_toMatrix', TensorProduct.LieModule.coe_liftLie_eq_lift_coe, InnerProductSpace.gramSchmidt_triangular, QuadraticAlgebra.basis_repr_apply, LinearMap.star_eq_adjoint, LinearMap.toMatrix_smulBasis_right, Matrix.toLpLin_symm_id, Matrix.range_toLin_eq_top, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, Matrix.toLin_finTwoProd_apply, Matrix.isPositive_toEuclideanLin_iff, RootPairing.coreflection_apply_self, ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap, RootPairing.polarizationEquiv_apply, NumberField.integralBasis_repr_apply, LinearMap.mul_toMatrix₂, TensorProduct.inner_assoc_assoc, kroneckerTMulLinearEquiv_mul, QuadraticMap.discr_comp, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, kroneckerTMulLinearEquiv_symm_kroneckerTMul, RootPairing.bijOn_coreflection_coroot, MultilinearMap.freeFinsuppEquiv_def, Rep.coindResAdjunction_homEquiv_apply, ZMod.invDFT_apply', LinearMap.toMatrix'_mul, LinearMap.adjoint_toSpanSingleton, mul_basis_toMatrix, Submodule.rTensorOne_tmul, LinearMap.toMatrix_algebraMap, LinearMap.spectrum_toMatrix, PowerBasis.constr_pow_gen, LinearMap.SeparatingRight.toMatrix₂, Matrix.isUnit_toLin_iff, Polynomial.degreeLT.addLinearEquiv_apply', Subspace.quotAnnihilatorEquiv_apply, Matrix.diagonal_toLin', LinearMap.re_inner_adjoint_mul_self_nonneg, TensorPower.mul_one, LinearMap.isPositive_self_comp_adjoint, QuadraticForm.tensorLId_symm_apply, Matrix.charpoly_toLin', Matrix.toLinearMap₂'_toMatrix', PiTensorProduct.ofFinsuppEquiv_apply, Matrix.toLinearMapₛₗ₂'_apply, TensorProduct.finsuppScalarRight_symm_apply_single, Algebra.Extension.H1Cotangent.equivOfFormallySmooth_apply, Matrix.toLin'_pow, RootPairing.IsOrthogonal.reflection_apply_right, LinearMap.BilinForm.SeparatingLeft.toMatrix, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, Complex.equivRealProdLm_symm_apply, Matrix.l2_opNNNorm_def, LinearMap.apply_toPerfPair_flip, apply_eq_star_dotProduct_toMatrix₂_mulVec, tensorKaehlerQuotKerSqEquiv_tmul_D, LinearMap.toMatrix_mul, Complex.coe_basisOneI_repr, LinearMap.toMatrix₂_compl₁₂, Matrix.minpoly_toLin', Representation.coind'_apply_apply, LinearMap.eq_adjoint_iff, GradedTensorProduct.mulHom_apply, BilinForm.toMatrix_compRight, LinearMap.BilinForm.nondegenerate_toMatrix'_iff, Module.DirectLimit.linearEquiv_symm_mk, LinearMap.toMatrix₂_toLinearMap₂, LinearMap.detAux_def', MultilinearMap.fromDirectSumEquiv_lof, TensorProduct.directSumRight_tmul_lof, LinearMap.toMatrix_transpose_apply', LinearMap.toMatrix'_intrinsicStar, QuadraticForm.tensorComm_apply, LinearEquiv.lieConj_apply, IsBaseChange.linearMapLeftRightHom_toMatrix, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, lsum_single, Matrix.toLinOfInv_symm_apply, LinearMap.toMatrix_smulRight, kroneckerTMulLinearEquiv_tmul, LinearMap.toMatrix₂Aux_eq, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, isAdjointPair_toLinearMap₂', RootPairing.Equiv.coweightMap_coweightEquiv_symm, Matrix.toLin'_apply', Representation.asModuleEquiv_symm_map_rho, RootPairing.Base.toCoweightBasis_repr_coroot, AdjoinRoot.powerBasisAux'_repr_symm_apply, RootPairing.reflectionPerm_eq_reflectionPerm_iff_of_span, ZMod.dft_comp_neg, TensorProduct.directSumLeft_symm_lof_tmul, Matrix.ker_toLin'_eq_bot_iff, Representation.ofModule_asModule_act, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LinearMap.SeparatingLeft.toMatrix₂, LinearMap.toMatrix'_toLinearMap₂', Basis.multilinearMap_apply_apply, PolynomialModule.equivPolynomial_single, BilinForm.toMatrix_mul_basis_toMatrix, WeakDual.isClosed_closedBall, LinearMap.BilinForm.mul_toMatrix', QuadraticForm.tensorAssoc_symm_apply, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, LinearMap.toMatrixRight'_id, LinearMap.minpoly_toMatrix, LinearMap.adjoint_lTensor, Matrix.nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, Module.reflection_mul_reflection_pow_apply_self, Submodule.rTensorOne_tmul_one, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, IsAdjoinRootMonic.coeff_apply_lt, LinearEquiv.map_dfinsuppSumAddHom, DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, Module.dualProdDualEquivDual_apply, Module.Basis.toMatrix_apply, RootPairing.Hom.weight_coweight_transpose_apply, KaehlerDifferential.mvPolynomialBasis_repr_apply, finsuppTensorFinsuppRid_single_tmul_single, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, SpecialLinearGroup.congr_linearEquiv_apply_apply, Algebra.toMatrix_lmul', toWeakSpace_closedConvexHull_eq, Algebra.Extension.contangentEquiv_tmul, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, TensorProduct.finsuppScalarLeft_apply_tmul_apply, Matrix.ker_diagonal_toLin', TensorProduct.inner_comm_comm, Module.AEval.of_symm_X_smul, FGModuleCat.Iso.conj_eq_conj, ZLattice.exists_forall_abs_repr_le_norm, Matrix.toBilin'_apply, LieAlgebra.conj_ad_apply, LinearMap.toMatrix_prodMap, Matrix.toLin_apply, Matrix.toLin'_one, Algebra.TensorProduct.linearEquivIncludeRange_symm_tmul, MultilinearMap.freeFinsuppEquiv_apply, ZMod.dft_dft, MultilinearMap.fromDirectSumEquiv_apply, Matrix.reindexLinearEquiv_mul, finsuppLEquivDirectSum_single, TensorProduct.assocIsometry_apply, Matrix.toLin_conjTranspose, GradedTensorProduct.auxEquiv_tmul, Ideal.cotangentEquivIdeal_apply, AdicCompletion.congr_symm_apply, LinearIsometryEquiv.rTensor_apply, PolynomialModule.equivPolynomialSelf_apply_eq, Polynomial.degreeLT.addLinearEquiv_symm_apply, PiTensorProduct.ofDFinsuppEquiv_tprod_single, DirectSum.decomposeLinearEquiv_apply, LinearMap.BilinForm.nondegenerate_congr_iff, exteriorPower.alternatingMapLinearEquiv_comp, Matrix.trace_toLin'_eq, TensorProduct.gradedComm_of_zero_tmul, Matrix.toLin'OfInv_symm_apply, Orientation.rotation_eq_matrix_toLin, Module.Basis.sumQuot_repr_inr_of_mem, AlternatingMap.domDomCongrₗ_toAddEquiv, QuadraticAlgebra.linearEquivTuple_symm_apply, Module.FinitePresentation.linearEquivMapExtendScalars_apply, IsBaseChange.endHom_apply, Module.Basis.parallelepiped_eq_map, TensorPower.algebraMap₀_mul_algebraMap₀, TensorPower.gMul_def, LinearEquiv.isUnit_det, LinearMap.polyCharpolyAux_map_aeval, TensorProduct.directSumLeft_tmul, Algebra.traceMatrix_of_basis, Trivialization.coordChangeL_symm_apply, SpecialLinearGroup.toLinearEquiv_symm_apply, NumberField.inverse_basisMatrix_mulVec_eq_repr, Matrix.spectrum_toLin, LinearMap.toMatrix'_comp, Matrix.toLinearEquiv'_apply, LinearMap.isUnit_toMatrix'_iff, Matrix.toBilin_toMatrix, IsBaseChange.toDual_apply, ZLattice.volume_image_eq_volume_div_covolume, RootPairing.reflection_apply_self, Module.AEval.mem_mapSubmodule_symm_apply, Matrix.nondegenerate_toLinearMap₂_iff, Matrix.reindexLinearEquiv_apply, Matrix.toBilin'_comp, Matrix.isHermitian_iff_isSymmetric, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', MultilinearMap.freeFinsuppEquiv_single, Module.AEval.X_smul_of, InnerProductSpace.toMatrix_rankOne, QuadraticForm.tmul_tensorLId_apply, PeriodPair.latticeEquiv_symm_apply, MvPolynomial.rTensor_symm_apply_single, CStarMatrix.reindexₗ_apply, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, QuadraticForm.tensorLId_apply, LinearMap.mul_toMatrix₂_mul, LinearMap.BilinForm.tensorDistribEquiv_tmul, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, LinearMap.eq_adjoint_iff_basis, QuotSMulTop.equivQuotTensor_naturality_mk, DirectSum.decomposeLinearEquiv_symm_apply, LinearMap.toMatrix'_id, LinearMap.polyCharpolyAux_coeff_eval, LinearMap.BilinForm.mul_toMatrix_mul, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, Matrix.toLinAlgEquiv_apply, LinearMap.nondegenerate_toMatrix₂'_iff, LinearMap.BilinForm.toMatrix'_comp, TensorProduct.equivFinsuppOfBasisRight_apply, WittVector.StandardOneDimIsocrystal.frobenius_apply, TensorProduct.directSum_symm_lof_tmul, Rep.coindResAdjunction_homEquiv_symm_apply, Matrix.toLinearMapRight'_apply, LinearMap.BilinForm.toMatrix_mul, Matrix.ofLp_toEuclideanLin_apply, Matrix.toLinearMap₂_apply, ZLattice.abs_repr_lt_of_norm_lt, Complex.coe_selfAdjointEquiv, MultilinearMap.freeDFinsuppEquiv_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply', LieAlgebra.LoopAlgebra.residuePairing_apply_apply, LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero, MvPolynomial.rTensor_apply_monomial_tmul, CoalgEquiv.coe_symm_toLinearEquiv, Algebra.Generators.repr_CotangentSpaceMap, lieEquivMatrix'_symm_apply, Matrix.proj_diagonal, Module.Dual.baseChange_baseChange, NumberField.mixedEmbedding.stdBasis_apply_isReal, ZMod.completedLFunction_one_sub_odd, LinearMap.isUnit_toMatrix_iff, TensorProduct.enorm_assoc, LinearMap.BilinForm.toMatrix_compLeft, LinearMap.trace_eq_matrix_trace, RootPairing.polarizationEquiv_symm_apply_coroot, BilinForm.toMatrix_apply, WeakDual.CharacterSpace.norm_le_norm_one, Matrix.linfty_opNorm_toMatrix, exteriorPower.zeroEquiv_ιMulti, LinearEquiv.transvection.coe_apply, Matrix.toBilin'_apply', Matrix.toLinearMap₂'_single, LinearMap.separatingRight_toLinearMap₂'_of_det_ne_zero', LinearMap.adjoint_inner_left, Polynomial.eval_eq_sum_degreeLTEquiv, LinearMap.BilinForm.mul_toMatrix, TensorProduct.finsuppScalarLeft_apply_tmul, TensorProduct.directSumRight_tmul, TensorProduct.gradedComm_tmul_algebraMap, LinearMap.trace_conj', Matrix.SpecialLinearGroup.toLin'_to_linearMap, ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv, TensorProduct.norm_lid, LinearMap.mul_toMatrix₂'_mul, LinearMap.toMatrix₂'_mul, ZLattice.volume_image_eq_volume_div_covolume', Algebra.toMatrix_lsmul, toMatrix_innerSL_apply, Matrix.separatingLeft_toLinearMap₂'_iff, exteriorPower.basis_repr_apply, LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero', Module.Basis.toMatrix_update, TensorPower.cast_tprod, PiLp.basis_toMatrix_basisFun_mul, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, BilinForm.toMatrix_mul, Rep.leftRegularHomEquiv_symm_single, LinearMap.toMatrix_comp, Module.reflection_mul_reflection_zpow_apply_self, RootPairing.coreflection_apply, PositiveLinearMap.ofPreGNS_toPreGNS, Matrix.separatingLeft_toBilin'_iff, Module.Basis.baseChange_repr_tmul, TensorProduct.nnnorm_assoc, Matrix.kroneckerAlgEquiv_symm_apply, Matrix.trace_toLin_eq, TensorPower.cast_eq_cast, LinearMap.toMatrix₂_mul_basis_toMatrix, ZSpan.repr_fract_apply, finsuppLEquivDirectSum_apply, Module.Basis.toMatrix_eq_toMatrix_constr, Matrix.det_reindexLinearEquiv_self, TensorProduct.comul_tmul, Algebra.TensorProduct.basis_repr_symm_apply, LinearMap.polyCharpoly_map_eq_charpoly, finsuppTensorFinsuppLid_apply_apply, Matrix.toLinOfInv_apply, dualTensorHomEquivOfBasis_symm_cancel_left, QuaternionAlgebra.coe_basisOneIJK_repr, QuadraticMap.IsometryEquiv.coe_toLinearEquiv, PiTensorProduct.liftIsometry_apply_apply, Submodule.FG.lTensor.directLimit_apply, Matrix.toBilin'Aux_eq, LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix', Matrix.toLin_finTwoProd_toContinuousLinearMap, Orientation.volumeForm_zero_neg, ZMod.dft_const_mul, TensorPower.one_mul, RootPairing.isFixedPt_reflection_of_isOrthogonal, LinearMap.linearEquivOfInjective_apply, PiTensorProduct.norm_eval_le_projectiveSeminorm, AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_apply, Module.reflection_mul_reflection_zpow_apply, TensorProduct.commIsometry_apply, finsuppTensorFinsupp_symm_single, Matrix.toLinearEquivRight'OfInv_apply, hasEigenvalue_toLin'_diagonal_iff, LinearMap.toMatrix'_toLinearMapₛₗ₂', LinearMap.isStarProjection_toContinuousLinearMap_iff, Rep.MonoidalClosed.linearHomEquiv_hom, Matrix.toLpLin_mul, Matrix.toLin'_submatrix, Derivation.compAEval_eq, Matrix.separatingLeft_toLinearMap₂_iff, Matrix.toLin_toMatrix, NumberField.mixedEmbedding.latticeBasis_repr_apply, Submodule.lTensorOne_symm_apply, LinearMap.toMatrix₂_apply, AdicCompletion.sumEquivOfFintype_apply, LinearMap.adjoint_comp, RootPairing.Equiv.weightEquiv_symm_weightMap, KaehlerDifferential.mvPolynomialBasis_repr_D, QuadraticForm.tensorAssoc_apply, RootPairing.coroot'_reflection, Matrix.toEuclideanLin_apply_piLp_toLp, Module.AEval.of_aeval_smul, Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply, finsuppTensorFinsuppRid_apply_apply, RootPairing.Base.toWeightBasis_repr_root, Algebra.leftMulMatrix_mulVec_repr, iSupIndep_iff_dfinsupp_lsum_injective, RootPairing.toPerfPair_conj_reflection, Module.Basis.parallelepiped_map, Polynomial.toMatrix_sylvesterMap, TensorProduct.finsuppRight_symm_apply_single, TensorProduct.gradedComm_one_tmul, Matrix.separatingRight_toBilin'_iff, Trivialization.coe_coordChangeL, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, Matrix.toLin_finTwoProd, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap, LinearMap.BilinForm.apply_toDual_symm_apply, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, LinearEquiv.charpoly_conj, Algebra.Generators.snd_cotangentCompLocalizationAwayEquiv, QuaternionAlgebra.coe_linearEquivTuple, finsuppTensorFinsuppLid_single_tmul_single, Matrix.kroneckerTMulAlgEquiv_apply, ZSpan.map_fundamentalDomain, LinearMap.nondegenerate_toMatrix₂_iff, MeasureTheory.Measure.addHaar_preimage_linearEquiv, Matrix.toLin_one, TensorAlgebra.mk_reindex_fin_cast, Matrix.toLin_transpose, GradedTensorProduct.of_symm_of, Complex.toMatrix_conjAe, BilinForm.mul_toMatrix, Matrix.toLpLin_symm_comp, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, Matrix.toLinearMapₛₗ₂_apply_basis, TensorProduct.finsuppLeft_apply_tmul, PiTensorProduct.ofFinsuppEquiv'_apply_apply, LinearMap.toMatrix_toSpanSingleton, RootPairing.toPerfPair_flip_conj_coreflection, Polynomial.degreeLT.addLinearEquiv_natAdd, Coalgebra.coassoc_apply, ZMod.invDFT_def, LinearMap.Nondegenerate.toMatrix₂', RootPairing.Equiv.reflection_smul, TensorProduct.equivFinsuppOfBasisRight_symm, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, exteriorPower.basis_repr, Submodule.lTensorOne_tmul, Matrix.Nondegenerate.toBilin', FDRep.Iso.conj_ρ, TensorProduct.directLimitLeft_tmul_of, LinearMap.toMatrix_singleton, LinearMap.BilinForm.toMatrix'_mul, Submodule.LinearDisjoint.val_mulMap_tmul, Algebra.traceMatrix_of_basis_mulVec, IsBaseChange.basis_repr_comp, exteriorPower.alternatingMapLinearEquiv_symm_apply, OrthonormalBasis.coe_toBasis_repr_apply, ZLattice.normBound_spec, LinearMap.toMatrix₂'_compl₂, TensorPower.mul_algebraMap₀, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, LieAlgebra.IsKilling.traceForm_coroot, IsAdjoinRootMonic.coeff_apply_coe, TensorProduct.nnnorm_comm, Ideal.cotangentEquivIdeal_symm_apply, Module.Basis.traceDual_repr_apply, TensorAlgebra.mk_reindex_cast, Matrix.nondegenerate_toLinearMap₂'_iff, LinearMap.separatingRight_toMatrix₂_iff, DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne, NumberField.Units.logEmbeddingEquiv_apply, RootPairing.coreflection_same, Module.Invertible.linearEquivOfRightInverse_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis, Module.Basis.ofZLatticeComap_repr_apply, TensorProduct.directLimitLeft_symm_of_tmul, LinearIsometryEquiv.norm_map', LinearMap.toMvPolynomial_eval_eq_apply, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, Module.Basis.toMatrix_transpose_apply, LinearMap.separatingLeft_toMatrix₂_iff, ContinuousLinearMap.toUniformConvergenceCLM_continuous, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, Representation.asModuleEquiv_map_smul, AdicCompletion.piEquivOfFintype_apply, Module.Basis.ofZLatticeBasis_repr_apply, DirectSum.linearEquivFunOnFintype_symm_single, LinearMap.BilinForm.toMatrix'_toBilin', PowerBasis.liftEquiv'_symm_apply_apply, PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod, PowerBasis.constr_pow_mul, StrongDual.coe_toWeakDual, LinearMap.det_toMatrix', Matrix.separatingLeft_toBilin_iff, WeakDual.toStrongDual_apply, LinearMap.eq_adjoint_iff_basis_right, LinearMap.Nondegenerate.toMatrix₂, LinearMap.toMatrixAlgEquiv_apply', Matrix.toLin'OfInv_apply, Basis.equivFun_symm_single, IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply, MvPolynomial.scalarRTensor_symm_apply_single, FractionalIdeal.equivNum_apply, TensorProduct.equivFinsuppOfBasisLeft_apply, LinearMap.BilinForm.Nondegenerate.toMatrix', Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inl, LinearMap.toMatrix_basis_equiv, Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inr, Matrix.reindexLinearEquiv_comp_apply, Matrix.SeparatingRight.toBilin', Matrix.kroneckerTMul_assoc, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, AffineIsometryEquiv.norm_map, Rep.diagonalHomEquiv_apply, LinearMap.coe_toContinuousLinearMap_symm, Matrix.range_diagonal, ZMod.completedLFunction_one_sub_even, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, Module.reflection_apply, BilinForm.toMatrix_compLeft, LinearMap.IsPositive.adjoint_eq, Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace, AdicCompletion.congr_apply, LinearMap.toPerfPair_apply, LinearMap.equivOfIsUnitDet_apply, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, LinearMap.toMatrix₂'_comp, MvPolynomial.rTensor_apply, RootPairing.IsOrthogonal.coreflection_apply_left, Matrix.toLinearMap₂_apply_basis, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, LinearMap.toMatrix_pow, IsBaseChange.linearMapLeftRightHom_apply, LinearMap.BilinForm.toMatrix_comp, Matrix.SpecialLinearGroup.toLin'_symm_apply, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, Module.Basis.continuous_coe_repr, TensorProduct.finsuppScalarLeft_apply, Submodule.lTensorOne_one_tmul, LinearMap.toMatrix'_one, KaehlerDifferential.tensorKaehlerEquiv_tmul_D, Module.surjective_piEquiv_apply_iff, LinearMap.transvection.congr, ZSpan.repr_floor_apply, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, PiTensorProduct.ofDirectSumEquiv_tprod_apply, LinearMap.tensorKerEquiv_apply, basis_toMatrix_mul_linearMap_toMatrix, LinearMap.toMatrixₛₗ₂'_apply, Submodule.mem_biSup_iff_exists_dfinsupp, Module.Basis.tensorProduct_repr_tmul_apply, PolynomialLaw.ground_apply, Matrix.toLinearMapRight'_one, Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift, Basis.piTensorProduct_repr_tprod_apply, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, TensorProduct.finsuppScalarLeft_symm_apply_single, Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix, Module.Basis.repr_smul', lmap_finsuppLEquivDirectSum_eq, RootPairing.reflection_apply, Matrix.toLpLin_apply, TensorProduct.congrIsometry_apply, ZMod.dft_eq_fourier, ZMod.dft_odd_iff, Matrix.toLin'_apply, LinearMap.BilinForm.SeparatingRight.toMatrix', ContinuousLinearMap.toUniformConvergenceCLM_symm_apply, Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero, LinearMap.toMatrix_adjoint, GradedTensorProduct.of_one, Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero, Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply, LinearMap.BilinForm.Nondegenerate.toMatrix, TensorProduct.nnnorm_lid, LinearMap.im_inner_adjoint_mul_self_eq_zero, Matrix.l2_opNorm_def, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, exteriorPower.oneEquiv_ιMulti, GradedTensorProduct.symm_of_of, Matrix.toEuclideanLin_toLp, LinearMap.toLinearMap_toPerfPair, RootPairing.coroot_reflectionPerm, TensorProduct.gradedComm_of_tmul_of, PowerBasis.constr_pow_aeval, LinearMap.det_toMatrix, Algebra.traceForm_toMatrix_powerBasis, Matrix.minpoly_toLin, basis_toMatrix_mul, Matrix.toLin'_toMatrix', LinearMap.det_toLin, Module.Basis.det_map, LinearMap.posSemidef_toMatrix_iff, ZMod.LFunction_dft, Module.Basis.norm_repr_le_norm, LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero', MvPolynomial.scalarRTensor_apply_tmul_apply, Derivation.compAEval_apply, Pi.basisFun_repr, Algebra.leftMulMatrix_eq_repr_mul, TensorProduct.directLimitRight_symm_of_tmul, FGModuleCat.Iso.conj_hom_eq_conj, LinearMap.SeparatingLeft.toMatrix₂', TensorProduct.toMatrix_comm, RootPairing.coreflection_apply_coroot, ZMod.dft_const_smul, ZSpan.mem_fundamentalDomain, dualTensorHomEquivOfBasis_apply, NormedSpace.Dual.coe_toWeakDual, LinearMap.toMatrix₂'_apply, Submodule.FG.rTensor.directLimit_apply', LinearMap.isAdjointPair_inner, LinearMap.IsPositive.adjoint_conj, Module.Basis.toMatrix_mulVec_repr, AdicCompletion.sumEquivOfFintype_symm_apply, Matrix.kroneckerStarAlgEquiv_apply, Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, LinearMap.BilinForm.separatingLeft_toMatrix_iff, TensorProduct.sum_tmul_basis_left_injective, ZMod.dft_smul_const, Module.AEval.mem_mapSubmodule_apply, TensorProduct.equivFinsuppOfBasisRight_symm_apply, Real.volume_preserving_transvectionStruct, ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT, Matrix.toBilin'_toMatrix', Module.Invertible.linearEquivOfLeftInverse_apply, Matrix.toLinearMapₛₗ₂_toMatrix₂, LinearMap.toMatrix'_mulVec, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range, IsBaseChange.toDualBaseChange_tmul, Matrix.SeparatingLeft.toLinearMap₂, hasEigenvector_toLin_diagonal, LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero, ZMod.dft_def, dotProduct_toMatrix₂_mulVec, TensorProduct.gradedComm_gradedMul, Matrix.diagonal_comp_single, LinearMap.toMatrixAlgEquiv_transpose_apply, AdicCompletion.piEquivFin_apply, NormedSpace.Dual.toWeakDual_inj, TensorProduct.finsuppRight_apply_tmul_apply, TensorProduct.directSumRight_symm_lof_tmul, LinearMap.traceAux_def, MultilinearMap.fromDFinsuppEquiv_symm_apply, Algebra.leftMulMatrix_apply, InnerProductSpace.symm_toEuclideanLin_rankOne, LinearMap.BilinForm.toMatrix'_compRight, TensorProduct.finsuppRight_apply_tmul, Polynomial.degreeLT.basis_repr, Matrix.SeparatingRight.toBilin, Module.reflection_mul_reflection_mul_reflection_pow_apply_self, LieModule.coe_maxTrivLinearMapEquivLieModuleHom, Module.reflection_mul_reflection_mul_reflection_zpow_apply_self, LinearMap.toMatrix_apply, RootPairing.mapsTo_coreflection_coroot, NumberField.house.basis_repr_norm_le_const_mul_house, TensorProduct.toMatrix_map, Matrix.rank_vecMulVec, ContinuousLinearMap.toWOT_apply, Submodule.coe_prodEquivOfClosedCompl, LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrixAlgEquiv_transpose_apply', RootPairing.root_reflectionPerm, LinearMap.toMatrixRight'_comp, PositiveLinearMap.preGNS_norm_sq, Matrix.kroneckerStarAlgEquiv_symm_apply, TensorProduct.assocIsometry_symm_apply, LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm, Matrix.toBilin_comp, TensorProduct.coe_finsuppScalarRight', LinearMap.polyCharpoly_coeff_eval, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj, DirectSum.linearEquivFunOnFintype_symm_coe, SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent, lsum_comp_mapRange_toSpanSingleton, Module.Basis.repr_unop_eq_mulOpposite_repr, LinearMap.det_toMatrix_eq_det_toMatrix, Algebra.TensorProduct.linearEquivIncludeRange_tmul, Matrix.SpecialLinearGroup.toLin'_apply, LinearMap.adjoint_id, exteriorPower.basis_repr_self, TensorProduct.finsuppLeft'_apply, GradedTensorProduct.of_symm_one, Submodule.coe_prodEquivOfClosedCompl_symm, TensorProduct.finsuppRight_tmul_single, Matrix.Nondegenerate.toLinearMap₂', finsuppLEquivDirectSum_symm_lof, Trivialization.linearEquivAt_symm_apply, Matrix.separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂, Module.Basis.sumQuot_repr_inr, ZMod.dft_apply_zero, Subspace.dualEquivDual_apply, ZLattice.abs_repr_le, DirectSum.IsInternal.collectedBasis_repr_of_mem, RootPairing.reflection_image_eq, DirectSum.coe_congrLinearEquiv, RootPairing.Equiv.coweightEquiv_apply, LinearMap.IsPositive.conj_adjoint, LinearMap.ker_toContinuousLinearMap, LinearMap.charpoly_toMatrix, LinearMap.isSymm_iff_isHermitian_toMatrix, Matrix.toBilin'_single, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply, LinearMap.toMatrix_toLin, TensorProduct.finsuppLeft_apply_tmul_apply, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, SpecialLinearGroup.toLinearEquiv_apply, Matrix.toLinearEquiv_apply, hasEigenvalue_toLin_diagonal_iff, RootPairing.reflection_apply_root, Matrix.spectrum_toLin', kroneckerLinearEquiv_tmul, MvPolynomial.rTensorAlgHom_apply_eq
lapply 📖	CompOp	6 math math: injective_pi_lapply, comul_comp_lapply, lapply_comp_lsingle_of_ne, lapply_apply, MultilinearMap.dfinsuppFamily_single_left, lapply_comp_lsingle_same
linearEquivFunOnFintype 📖	CompOp	3 math math: MultilinearMap.freeDFinsuppEquiv_def, linearEquivFunOnFintype_symm_apply, linearEquivFunOnFintype_apply
lmk 📖	CompOp	—
lsingle 📖	CompOp	14 math math: comul_single, lsum_lsingle, lsingle_apply, MultilinearMap.dfinsuppFamily_compLinearMap_lsingle, iSup_range_lsingle, counit_comp_lsingle, MultilinearMap.dfinsupp_ext_iff, comul_comp_lsingle, lsum_symm_apply, lapply_comp_lsingle_of_ne, MultilinearMap.dfinsuppFamily_single_left, lapply_comp_lsingle_same, MultilinearMap.fromDFinsuppEquiv_symm_apply, lhom_ext'_iff
lsum 📖	CompOp	12 math math: iSupIndep.dfinsupp_lsum_injective, lsum_lsingle, Submodule.biSup_eq_range_dfinsupp_lsum, sum_mapRange_index.linearMap, Submodule.mem_iSup_iff_exists_dfinsupp, Submodule.iSup_eq_range_dfinsupp_lsum, lsum_single, lsum_symm_apply, iSupIndep_iff_dfinsupp_lsum_injective, Submodule.mem_biSup_iff_exists_dfinsupp, lsum_apply_apply, lsum_comp_mapRange_toSpanSingleton
sigmaCurryLEquiv 📖	CompOp	3 math math: sigmaCurryLEquiv_apply, MultilinearMap.freeDFinsuppEquiv_def, sigmaCurryLEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprodMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module LinearMap.instFunLike coprodMap sum mapRange map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass RingHom RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass	—	sumAddHom_apply
coprodMap_apply_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module LinearMap.instFunLike coprodMap single	—	RingHomInvPair.ids mapRange_single sumAddHom_single
domLCongr_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm addCommMonoid module LinearEquiv.instEquivLike domLCongr comapDomain' Equiv.right_inv	—	RingHomInvPair.ids
iSup_range_lsingle 📖	mathematical	—	iSup Submodule DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle Top.top Submodule.instTop	—	RingHomSurjective.ids top_le_iff LinearMap.id_apply RingHomInvPair.ids smulCommClass AddMonoid.nat_smulCommClass' lsum_lsingle dfinsuppSumAddHom_mem Submodule.addSubmonoidClass Submodule.mem_iSup_of_mem
injective_pi_lapply 📖	mathematical	—	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid Pi.addCommMonoid module Pi.module LinearMap.instFunLike LinearMap.pi lapply	—	ext
ker_mapRangeAddMonoidHom 📖	mathematical	—	AddMonoidHom.ker DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddGroup AddCommMonoid.toAddMonoid addZeroClass mapRange.addMonoidHom AddSubgroup.comap Pi.addGroup coeFnAddMonoidHom AddSubgroup.pi Set.univ	—	AddSubgroup.toAddSubmonoid_injective mker_mapRangeAddMonoidHom
ker_mapRangeLinearMap 📖	mathematical	—	LinearMap.ker DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module RingHom.id Semiring.toNonAssocSemiring mapRange.linearMap Submodule.comap Pi.addCommMonoid Pi.module coeFnLinearMap Submodule.pi Set.univ	—	Submodule.toAddSubmonoid_injective mker_mapRangeAddMonoidHom
lapply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module LinearMap.instFunLike lapply instDFunLike	—	—
lapply_comp_lsingle_of_ne 📖	mathematical	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lapply lsingle LinearMap LinearMap.instZero	—	LinearMap.ext RingHomCompTriple.ids single_apply
lapply_comp_lsingle_same 📖	mathematical	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lapply lsingle LinearMap.id	—	LinearMap.ext RingHomCompTriple.ids single_apply
lhom_ext 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module LinearMap.instFunLike single	—	—	LinearMap.toAddMonoidHom_injective addHom_ext
lhom_ext' 📖	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lsingle	—	—	RingHomCompTriple.ids lhom_ext LinearMap.congr_fun
lhom_ext'_iff 📖	mathematical	—	LinearMap.comp DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lsingle	—	RingHomCompTriple.ids lhom_ext'
linearEquivFunOnFintype_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid Pi.addCommMonoid module Pi.module EquivLike.toFunLike LinearEquiv.instEquivLike linearEquivFunOnFintype instDFunLike	—	RingHomInvPair.ids
linearEquivFunOnFintype_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid addCommMonoid Pi.module module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquivFunOnFintype Equiv Equiv.instEquivLike Equiv.symm equivFunOnFintype	—	RingHomInvPair.ids
lmk_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid Set.Elem SetLike.coe Finset Finset.instSetLike Set Set.instMembership addCommMonoid Pi.module module LinearMap.instFunLike	—	—
lsingle_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module LinearMap.instFunLike lsingle single	—	—
lsum_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike lsum AddMonoidHom addZeroClass AddMonoidHom.instFunLike sumAddHom LinearMap.toAddMonoidHom	—	RingHomInvPair.ids
lsum_lsingle 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap DFinsupp addCommMonoid module Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module smulCommClass EquivLike.toFunLike instEquivLikeLinearEquiv lsum lsingle LinearMap.id	—	lhom_ext RingHomInvPair.ids smulCommClass lsum_single
lsum_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module EquivLike.toFunLike instEquivLikeLinearEquiv lsum single	—	RingHomInvPair.ids sumAddHom_single
lsum_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module LinearMap.addCommMonoid Pi.addCommMonoid LinearMap.module Pi.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm lsum LinearMap.comp lsingle	—	RingHomInvPair.ids
mapRange_smul 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	mapRange DFinsupp instZero instSMulZeroClass	—	ext
mker_mapRangeAddMonoidHom 📖	mathematical	—	AddMonoidHom.mker DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addZeroClass AddMonoidHom AddMonoidHom.instFunLike AddMonoidHom.instAddMonoidHomClass mapRange.addMonoidHom AddSubmonoid.comap Pi.addZeroClass coeFnAddMonoidHom AddSubmonoid.pi Set.univ	—	AddSubmonoid.ext AddMonoidHom.instAddMonoidHomClass
mrange_mapRangeAddMonoidHom 📖	mathematical	—	AddMonoidHom.mrange DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addZeroClass AddMonoidHom AddMonoidHom.instFunLike AddMonoidHom.instAddMonoidHomClass mapRange.addMonoidHom AddSubmonoid.comap Pi.addZeroClass coeFnAddMonoidHom AddSubmonoid.pi Set.univ	—	AddSubmonoid.ext AddMonoidHom.instAddMonoidHomClass ext mk_of_mem notMem_support_iff mk_of_notMem map_zero AddMonoidHomClass.toZeroHomClass Set.mem_univ
range_mapRangeAddMonoidHom 📖	mathematical	—	AddMonoidHom.range DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddGroup mapRange.addMonoidHom AddSubgroup.comap Pi.addGroup coeFnAddMonoidHom AddSubgroup.pi Set.univ	—	AddSubgroup.toAddSubmonoid_injective mrange_mapRangeAddMonoidHom
range_mapRangeLinearMap 📖	mathematical	—	LinearMap.range DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mapRange.linearMap Submodule.comap Pi.addCommMonoid Pi.module coeFnLinearMap Submodule.pi Set.univ	—	Submodule.toAddSubmonoid_injective RingHomSurjective.ids mrange_mapRangeAddMonoidHom
sigmaCurryLEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instZero addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike sigmaCurryLEquiv Equiv Equiv.instEquivLike sigmaCurryEquiv	—	RingHomInvPair.ids
sigmaCurryLEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instZero addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm sigmaCurryLEquiv Equiv Equiv.instEquivLike Equiv.symm sigmaCurryEquiv	—	RingHomInvPair.ids

DFinsupp.mapRange

Definitions

Name	Category	Theorems
linearEquiv 📖	CompOp	4 math math: linearEquiv_refl, linearEquiv_trans, linearEquiv_symm, linearEquiv_apply
linearMap 📖	CompOp	7 math math: linearMap_comp, DFinsupp.range_mapRangeLinearMap, DFinsupp.sum_mapRange_index.linearMap, DFinsupp.ker_mapRangeLinearMap, linearMap_id, linearMap_apply, lsum_comp_mapRange_toSpanSingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike linearEquiv DFinsupp.mapRange DFinsupp.instEquivLikeLinearEquiv	—	RingHomInvPair.ids
linearEquiv_refl 📖	mathematical	—	linearEquiv LinearEquiv.refl DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module	—	LinearEquiv.ext RingHomInvPair.ids DFinsupp.mapRange_id
linearEquiv_symm 📖	mathematical	—	LinearEquiv.symm DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids linearEquiv	—	RingHomInvPair.ids
linearEquiv_trans 📖	mathematical	—	linearEquiv LinearEquiv.trans RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module	—	RingHomInvPair.ids LinearEquiv.ext RingHomCompTriple.ids DFinsupp.mapRange_comp LinearEquiv.map_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
linearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module LinearMap.instFunLike linearMap DFinsupp.mapRange	—	—
linearMap_comp 📖	mathematical	—	linearMap LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module	—	LinearMap.ext RingHomCompTriple.ids DFinsupp.mapRange_comp LinearMap.map_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
linearMap_id 📖	mathematical	—	linearMap LinearMap.id DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module	—	LinearMap.ext DFinsupp.ext

DFinsupp.sum_mapRange_index

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearMap 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module LinearMap.instFunLike LinearEquiv Nat.instSemiring RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum DFinsupp.mapRange.linearMap LinearMap.comp RingHomCompTriple.ids	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass' RingHomCompTriple.ids DFinsupp.sumAddHom_apply DFinsupp.sum_mapRange_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_dfinsuppSumAddHom 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv AddMonoidHom DFinsupp AddZero.toZero AddZeroClass.toAddZero DFinsupp.addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike DFinsupp.sumAddHom AddMonoidHom.comp AddEquiv.toAddMonoidHom toAddEquiv	—	AddEquiv.map_dfinsuppSumAddHom

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_dfinsuppSum 📖	mathematical	—	DFunLike.coe LinearMap instFunLike DFinsupp.sum addCommMonoid	—	—
dfinsuppSum_apply 📖	mathematical	—	DFunLike.coe LinearMap instFunLike DFinsupp.sum addCommMonoid	—	sum_apply
map_dfinsuppSumAddHom 📖	mathematical	—	DFunLike.coe LinearMap instFunLike AddMonoidHom DFinsupp AddZero.toZero AddZeroClass.toAddZero DFinsupp.addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike DFinsupp.sumAddHom AddMonoidHom.comp toAddMonoidHom	—	AddMonoidHom.map_dfinsuppSumAddHom

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biSup_eq_range_dfinsupp_lsum 📖	mathematical	—	iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice LinearMap.range DFinsupp SetLike.instMembership setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid DFinsupp.addCommMonoid DFinsupp.module module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.comp RingHomCompTriple.ids DFunLike.coe LinearEquiv Nat.instSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum subtype DFinsupp.filterLinearMap	—	le_antisymm RingHomSurjective.ids RingHomCompTriple.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' iSup₂_le LinearMap.comp_apply DFinsupp.filterLinearMap_apply DFinsupp.filter_single_pos DFinsupp.sumAddHom_single dfinsuppSumAddHom_mem mem_iSup_of_mem iSup_congr_Prop iSup_pos iSup_neg AddSubmonoidClass.toZeroMemClass addSubmonoidClass
dfinsuppSumAddHom_mem 📖	mathematical	Submodule SetLike.instMembership setLike DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike DFinsupp AddZero.toZero DFinsupp.instDFunLike	DFinsupp.addZeroClass DFinsupp.sumAddHom	—	dfinsuppSumAddHom_mem addSubmonoidClass
dfinsuppSum_mem 📖	mathematical	Submodule SetLike.instMembership setLike DFunLike.coe DFinsupp DFinsupp.instDFunLike	DFinsupp.sum	—	dfinsuppSum_mem addSubmonoidClass
iSup_eq_range_dfinsupp_lsum 📖	mathematical	—	iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice LinearMap.range DFinsupp SetLike.instMembership setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid DFinsupp.addCommMonoid DFinsupp.module module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearEquiv Nat.instSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum subtype	—	le_antisymm RingHomSurjective.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' iSup_le DFinsupp.sumAddHom_single dfinsuppSumAddHom_mem le_iSup
mem_biSup_iff_exists_dfinsupp 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid DFinsupp.addCommMonoid DFinsupp.module module LinearMap.instFunLike LinearEquiv Nat.instSemiring RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum subtype DFinsupp.filter	—	RingHomSurjective.ids RingHomCompTriple.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' SetLike.ext_iff biSup_eq_range_dfinsupp_lsum
mem_iSup_finset_iff_exists_sum 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Finset Finset.instMembership Finset.sum	—	mem_iSup_iff_exists_dfinsupp' iSup_const_le coe_mem Finset.sum_subset Mathlib.Tactic.Contrapose.contrapose₁ DFinsupp.mem_support_iff not_ne_iff coe_zero mem_bot iSup_neg iSup_pos Finset.sum_congr DFinsupp.support_mk_subset DFinsupp.mk_of_mem
mem_iSup_iff_exists_dfinsupp 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid DFinsupp.addCommMonoid DFinsupp.module module LinearMap.instFunLike LinearEquiv Nat.instSemiring RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum subtype	—	RingHomSurjective.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' SetLike.ext_iff iSup_eq_range_dfinsupp_lsum
mem_iSup_iff_exists_dfinsupp' 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice DFinsupp.sum zero	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass' mem_iSup_iff_exists_dfinsupp DFinsupp.sumAddHom_apply
mem_iSup_iff_exists_finsupp 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike Finsupp.sum	—	mem_iSup_iff_exists_dfinsupp' AddSubmonoidClass.toZeroMemClass addSubmonoidClass Finset.sum_congr Finset.ext Finsupp.mem_support_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSupIndep_iff_dfinsuppSumAddHom_injective 📖	mathematical	—	iSupIndep AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instCompleteLattice DFinsupp SetLike.instMembership AddSubgroup.instSetLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DFunLike.coe AddMonoidHom DFinsupp.addZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid AddMonoidHom.instFunLike DFinsupp.sumAddHom AddSubgroup.subtype	—	iSupIndep.dfinsuppSumAddHom_injective iSupIndep_of_dfinsuppSumAddHom_injective'
iSupIndep_iff_dfinsupp_lsum_injective 📖	mathematical	—	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice DFinsupp SetLike.instMembership Submodule.setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.addCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp.addCommMonoid DFinsupp.module Submodule.module LinearMap.instFunLike LinearEquiv Nat.instSemiring RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum Submodule.subtype	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass' iSupIndep.dfinsupp_lsum_injective iSupIndep_of_dfinsupp_lsum_injective
iSupIndep_iff_finset_sum_eq_imp_eq 📖	mathematical	—	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice	—	iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero Finset.sum_congr Finset.sum_sub_distrib Submodule.sub_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Finset.sum_const_zero
iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero 📖	mathematical	—	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Submodule.neg_mem_iff add_eq_zero_iff_neg_eq Finset.add_sum_erase SetLike.le_def instIsConcreteLE biSup_mono Submodule.sum_mem_biSup Submodule.mem_iSup_iff_exists_finsupp Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Submodule.neg_mem iSup_congr_Prop iSup_pos iSup_neg
iSupIndep_iff_forall_dfinsupp 📖	mathematical	—	iSupIndep Submodule Submodule.completeLattice SetLike.instMembership Submodule.setLike Submodule.zero	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass' DFinsupp.filter_ne_eq_erase Subtype.forall'
iSupIndep_iff_linearIndependent_of_ne_zero 📖	mathematical	—	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice Submodule.span Set Set.instSingletonSet LinearIndependent	—	iSupIndep.linearIndependent Submodule.mem_span_singleton_self LinearIndependent.iSupIndep_span_singleton
iSupIndep_of_dfinsuppSumAddHom_injective 📖	mathematical	DFinsupp AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddZero.toZero AddZeroClass.toAddZero AddSubmonoid.toAddZeroClass DFunLike.coe AddMonoidHom DFinsupp.addZeroClass AddMonoidHom.instFunLike DFinsupp.sumAddHom AddSubmonoid.subtype	iSupIndep AddSubmonoid.instCompleteLattice	—	iSupIndep_map_orderIso_iff iSupIndep_of_dfinsupp_lsum_injective
iSupIndep_of_dfinsuppSumAddHom_injective' 📖	mathematical	DFinsupp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DFunLike.coe AddMonoidHom DFinsupp.addZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid AddMonoidHom.instFunLike DFinsupp.sumAddHom AddSubgroup.subtype	iSupIndep AddSubgroup.instCompleteLattice	—	iSupIndep_map_orderIso_iff iSupIndep_of_dfinsupp_lsum_injective
iSupIndep_of_dfinsupp_lsum_injective 📖	mathematical	DFinsupp Submodule SetLike.instMembership Submodule.setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.addCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp.addCommMonoid DFinsupp.module Submodule.module LinearMap.instFunLike LinearEquiv Nat.instSemiring RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum Submodule.subtype	iSupIndep Submodule.completeLattice	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass' iSupIndep_iff_forall_dfinsupp DFinsupp.lsum_single DFunLike.ext_iff DFinsupp.single_apply
lsum_comp_mapRange_toSpanSingleton 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFinsupp Submodule.addCommMonoid Finsupp.instAddCommMonoid DFinsupp.addCommMonoid Finsupp.module Semiring.toModule DFinsupp.module Submodule.module RingHom.id RingHomCompTriple.ids DFunLike.coe LinearEquiv Nat.instSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum Submodule.subtype DFinsupp.mapRange.linearMap LinearMap.toSpanSingleton LinearEquiv.toLinearMap finsuppLequivDFinsupp Finsupp.linearCombination	—	Finsupp.lhom_ext' RingHomCompTriple.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' LinearMap.ext_ring SMulMemClass.smul_mem Submodule.smulMemClass one_smul Finsupp.toDFinsupp_single DFinsupp.mapRange_single DFinsupp.sumAddHom_single Finsupp.linearCombination_single

iSupIndep

Definitions

Name	Category	Theorems
linearEquiv 📖	CompOp	2 math math: linearEquiv_symm_apply, linearEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dfinsuppSumAddHom_injective 📖	mathematical	iSupIndep AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instCompleteLattice	DFinsupp SetLike.instMembership AddSubgroup.instSetLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DFunLike.coe AddMonoidHom DFinsupp.addZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid AddMonoidHom.instFunLike DFinsupp.sumAddHom AddSubgroup.subtype	—	dfinsupp_lsum_injective iSupIndep_map_orderIso_iff
dfinsupp_lsum_injective 📖	mathematical	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice	DFinsupp SetLike.instMembership Submodule.setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.addCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DFinsupp.addCommMonoid DFinsupp.module Submodule.module LinearMap.instFunLike LinearEquiv Nat.instSemiring RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.module LinearMap.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DFinsupp.lsum Submodule.subtype	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass' LinearMap.ker_eq_bot' DFinsupp.ext DFinsupp.zero_apply neg_eq_zero iSupIndep_iff_forall_dfinsupp AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass Submodule.coe_neg add_eq_zero_iff_eq_neg Submodule.subtype_apply DFinsupp.lsum_single map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass DFinsupp.erase_add_single LinearMap.ker_eq_bot
linearEquiv_apply 📖	mathematical	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Top.top Submodule.instTop	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp SetLike.instMembership Submodule.setLike Submodule.zero DFinsupp.addCommMonoid Submodule.addCommMonoid DFinsupp.module Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike linearEquiv AddMonoidHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addZeroClass AddMonoidHom.instFunLike DFinsupp.sumAddHom LinearMap.toAddMonoidHom Submodule.subtype	—	RingHomInvPair.ids
linearEquiv_symm_apply 📖	mathematical	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Top.top Submodule.instTop SetLike.instMembership Submodule.setLike	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp Submodule.zero DFinsupp.addCommMonoid Submodule.addCommMonoid DFinsupp.module Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearEquiv DFinsupp.single	—	RingHomInvPair.ids DFinsupp.sumAddHom_single
linearIndependent 📖	mathematical	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice SetLike.instMembership Submodule.setLike	LinearIndependent	—	linearIndependent_iff dfinsupp_lsum_injective RingHomCompTriple.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' lsum_comp_mapRange_toSpanSingleton Finsupp.ext smul_left_injective IsDomain.toIsCancelMulZero zero_smul

---

← Back to Index