Defs

📁 Source: Mathlib/Algebra/Module/Equiv/Defs.lean

Statistics

Metric	Count
Definitions LinearEquiv, apply, symm_apply, cast, instCoeLinearMap, instEquivLike, instSMulUnitsId, invFun, ofInvolutive, refl, symmEquiv, aux, toAddEquiv, toEquiv, toLinearMap, trans, transNotation, LinearEquivClass, toSemilinearEquiv, SemilinearEquivClass, instCoeToSemilinearEquiv, semilinearEquiv, «term_≃ₗ[_]_», «term_≃ₛₗ[_]_»	24
Theorems apply_symm_apply, bijective, cast_apply, cast_symm_apply, coe_addEquiv_apply, coe_coe, coe_injective, coe_mk, coe_ofInvolutive, coe_symm_mk, coe_symm_mk', coe_symm_toEquiv, coe_toAddEquiv, coe_toAddEquiv_symm, coe_toEquiv, coe_toEquiv_symm, coe_toLinearMap, coe_trans, comp_coe, comp_symm, comp_symm_assoc, comp_symm_cancel_left, comp_symm_cancel_right, comp_symm_eq, comp_toLinearMap_eq_iff, comp_toLinearMap_symm_eq, congr_arg, congr_fun, eq_comp_symm, eq_comp_toLinearMap_iff, eq_comp_toLinearMap_symm, eq_symm_apply, eq_symm_comp, eq_toLinearMap_symm_comp, ext, ext_iff, image_eq_preimage_symm, image_symm_eq_preimage, injective, instSemilinearEquivClass, invFun_eq_symm, left_inv, map_add, map_eq_zero_iff, map_ne_zero_iff, map_smul, map_smulₛₗ, map_zero, mk_coe, mk_coe', refl_apply, refl_symm, refl_toLinearMap, refl_trans, right_inv, self_trans_symm, smul_apply, smul_trans, surjective, symmEquiv_apply_apply, symmEquiv_apply_symm_apply, symmEquiv_symm_apply_apply, symmEquiv_symm_apply_symm_apply, symm_apply_apply, symm_apply_eq, symm_bijective, symm_comp, symm_comp_assoc, symm_comp_cancel_left, symm_comp_cancel_right, symm_comp_eq, symm_mk, symm_smul, symm_smul_apply, symm_symm, symm_trans_apply, symm_trans_cancel_left, symm_trans_cancel_right, symm_trans_self, toAddMonoidHom_commutes, toEquiv_inj, toEquiv_injective, toEquiv_symm, toFun_eq_coe, toLinearMap_eq_coe, toLinearMap_inj, toLinearMap_injective, toLinearMap_smul, toLinearMap_symm_comp_eq, trans_apply, trans_assoc, trans_refl, trans_smul, trans_symm, trans_symm_cancel_left, trans_symm_cancel_right, toSemilinearEquiv_apply, toSemilinearEquiv_symm_apply, instSemilinearMapClass, map_smulₛₗ, semilinearEquiv_apply, toAddEquivClass	102
Total	126

LinearEquiv

Definitions

Name	Category	Theorems
cast 📖	CompOp	2 math math: cast_symm_apply, cast_apply
instCoeLinearMap 📖	CompOp	—
instEquivLike 📖	CompOp	792 math math: multilinearMapCongrLeft_symm_apply, MultilinearMap.domDomCongrLinearEquiv'_symm_apply, continuous_decomposeProdAdjoint, LieModule.shiftedGenWeightSpace.shift_apply, Finsupp.snd_sumFinsuppLEquivProdFinsupp, Rep.resCoindHomEquiv_symm_apply_hom, coe_toEquiv, Rep.resCoindHomEquiv_apply_hom, IsLocalizedModule.iso_symm_apply', Finsupp.fst_sumFinsuppLEquivProdFinsupp, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, Module.Basis.equivFun_self, Module.Basis.coe_map, Submodule.topEquiv_symm_apply_coe, PiTensorProduct.lift_reindex, multilinearMapCongrRight_apply, PiTensorProduct.lift.tprod, Module.Basis.end_repr_apply, Pretrivialization.linearEquivAt_symm_apply, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, ofBijective_symm_apply_apply, restrictScalars_apply, TensorProduct.AlgebraTensorModule.rid_symm_apply, PiTensorProduct.liftAlgHom_apply, coe_toAddEquiv, AlternatingMap.constLinearEquivOfIsEmpty_symm_apply, LinearMap.Nondegenerate.congr, PiTensorProduct.tmulEquiv_symm_apply, dotProductEquiv_symm_apply, piCongrRight_apply, addMonoidHomLequivNat_symm_apply, PiTensorProduct.isEmptyEquiv_apply_tprod, PiTensorProduct.dualDistribEquivOfBasis_symm_apply, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, Module.Basis.equivFun_symm_apply, AddEquiv.toIntLinearEquiv_toAddEquiv, TensorProduct.congr_congr, LinearMap.rTensor_comm, addMonoidHomLequivInt_apply, Module.DualBases.basis_repr_symm_apply, Module.Basis.constr_comp, Module.Basis.constr_symm_apply, Algebra.Extension.H1Cotangent.equiv_apply, Finsupp.sumFinsuppLEquivProdFinsupp_apply, Finsupp.supportedEquivFinsupp_symm_single, PiTensorProduct.lift_reindex_symm, PiTensorProduct.map_reindex_symm, WithLp.coe_linearEquiv, Module.Basis.dualBasis_coord_toDualEquiv_apply, Submodule.prodEquivOfIsCompl_symm_apply_snd_eq_zero, AlternatingMap.constLinearEquivOfIsEmpty_apply, PiTensorProduct.reindex_reindex, mapMatrix_apply, PiTensorProduct.subsingletonEquiv_symm_apply, Matrix.liftLinear_single, MulOpposite.coe_opLinearEquiv_symm, coe_mk, TensorProduct.piScalarRight_symm_algebraMap, LinearMap.BilinForm.congr_apply, CategoryTheory.InducedCategory.homLinearEquiv_apply, restrictScalars_symm_apply, TensorProduct.AlgebraTensorModule.rid_tmul, domMulActCongrRight_symm_apply, conj_apply_apply, Algebra.IsPushout.cancelBaseChange_tmul, skewSwap_symm_apply, TensorProduct.tensorTensorTensorComm_tmul, coe_withLpCongr, TensorProduct.AlgebraTensorModule.congr_symm_tmul, conjAlgEquiv_symm_apply_apply, Module.Basis.mk_repr, starLinearEquiv_symm_apply, Finsupp.linearEquivFunOnFinite_symm_coe, Module.Basis.repr_isUnitSMul, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply, ContinuousLinearMap.coprodEquiv_apply, map_mem_invtSubmodule_conj_iff, ModuleCat.Iso.homCongr_eq_arrowCongr, AlgEquiv.linearEquivConj_mulLeft, congrRight₂_apply, Shrink.linearEquiv_symm_apply, ULift.moduleEquiv_symm_apply, Module.Basis.prod_repr_inl, cast_symm_apply, ContinuousMultilinearMap.piLinearEquiv_symm_apply, SemimoduleCat.Iso.homCongr_eq_arrowCongr, IsLocalizedModule.iso_symm_apply, TensorProduct.AlgebraTensorModule.rightComm_symm_tmul, Algebra.IsPushout.cancelBaseChange_symm_tmul, Fintype.linearIndependent_iff', piFinTwo_symm_apply, Module.Basis.repr_self_apply, coe_inv, IsLocalizedModule.iso_apply_mk, bijective, LocallyConstant.congrRightₗ_symm_apply_apply, MultilinearMap.currySumEquiv_apply, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, LinearMap.sum_repr_mul_repr_mulₛₗ, LinearMap.ringLmapEquivSelf_symm_apply, Module.Basis.equiv_apply, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, FourierTransform.fourierEquiv_apply, LinearMap.separatingRight_congr_iff, Derivation.linearEquiv_coe_to_linearMap_comp, Submodule.quotEquivOfEqBot_symm_apply, Module.Relations.Solution.IsPresentation.linearEquiv_symm_var, MulOpposite.coe_opLinearEquiv_symm_addEquiv, conj_comp, domMulActCongrRight_apply, Rep.coinvariantsTensorFreeLEquiv_symm_apply, piCurry_apply, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply, Finsupp.curryLinearEquiv_symm_apply_apply, Finsupp.llift_apply, coe_symm_toEquiv, conj_refl, Module.Basis.toDualEquiv_apply, map_zero, dotProductEquiv_apply_apply, congrLeft_symm_apply, TensorProduct.leftComm_tmul, symm_apply_eq, TensorProduct.comm_comm, Module.Basis.repr_algebraMap, Matrix.liftLinear_singleLinearMap, Submodule.equivSubtypeMap_symm_apply, Submodule.botEquivPUnit_apply, Matrix.liftLinear_comp_singleLinearMap, LinearMap.prodEquiv_apply, WithConv.symm_linearEquiv_apply, Matrix.toLinearEquivRight'OfInv_symm_apply, eq_symm_apply, LinearMap.BilinForm.congr_comp, Finsupp.LinearEquiv.finsuppUnique_symm_apply, MultilinearMap.domDomCongrLinearEquiv_symm_apply, AddEquiv.toNatLinearEquiv_toAddEquiv, coe_curry, PositiveLinearMap.leftMulMapPreGNS_apply, image_symm_eq_preimage, PiTensorProduct.reindex_comp_tprod, Submodule.coe_prodEquivOfIsCompl', Module.Basis.ofEquivFun_repr_apply, ofSubmodules_apply, Submodule.topEquiv_apply, Module.Relations.Solution.IsPresentation.linearEquiv_apply, Module.Basis.reindexRange_repr', Module.Basis.reindexRange_repr, DistribMulAction.toLinearEquiv_symm_apply, ModuleCat.homLinearEquiv_symm_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, MultilinearMap.curryFinFinset_apply, IsNoetherian.equivPUnitOfProdInjective_apply, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, SemimoduleCat.homLinearEquiv_apply, LinearMap.IsProj.eq_conj_prodMap, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, ModularGroup.lcRow0Extend_symm_apply, LinearMap.extendScalarsOfIsLocalizationEquiv_apply, skewSwap_apply, arrowCongr_symm_apply, MulOpposite.coe_opLinearEquiv_addEquiv, Matrix.conjTransposeLinearEquiv_apply, PiTensorProduct.subsingletonEquiv_apply_tprod, uniqueProd_apply, DFinsupp.sigmaCurryLEquiv_apply, Finsupp.mapDomain.coe_linearEquiv, LocallyConstant.congrRightₗ_apply_apply, Module.Invertible.rTensorEquiv_apply_apply, Rep.coindVEquiv_symm_apply_coe, lTensor_tmul, coe_neg, TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul, basisOfLinearIndependentOfCardEqFinrank_repr_apply, LinearMap.lsum_apply, funUnique_symm_apply, LinearMap.toLinearMap_toContPerfPair, continuous_decomposeProdAdjoint_symm, Matrix.piLinearEquiv_apply, PiTensorProduct.congr_symm_tprod, ExteriorAlgebra.liftAlternatingEquiv_apply, coe_pow, TensorProduct.prodLeft_tmul, ofLeftInverse_symm_apply, isOpenMap_toWeakSpace_symm, KaehlerDifferential.linearMapEquivDerivation_apply_apply, comp_symm_eq, Submodule.botEquivPUnit_symm_apply, TensorProduct.map_map_assoc_symm, Module.Basis.addSubgroupOfClosure_repr_apply, KaehlerDifferential.tensorKaehlerEquivBase_symm_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply, Finsupp.linearEquivFunOnFinite_symm_apply, mul_apply, multilinearMapCongrRight_symm_apply, piUnique_symm_apply, MultilinearMap.coe_currySumEquiv_symm, eq_symm_comp, IsTensorProduct.equiv_symm_apply, MultilinearMap.curryFinFinset_symm_apply_piecewise_const, Module.Basis.reindexRange_repr_self, ofSubmodule'_symm_apply, surjective, TensorProduct.prodLeft_symm_tmul, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply, rTensor_refl_apply, KaehlerDifferential.linearMapEquivDerivation_symm_apply, piUnique_apply, sumPiEquivProdPi_apply, invFun_eq_symm, CliffordAlgebra.changeFormEquiv_apply, TensorProduct.dualDistribEquivOfBasis_symm_apply, IsLocalizedModule.linearEquiv_apply, LinearMap.quotientInfEquivSupQuotient_apply_mk, sumArrowLequivProdArrow_symm_apply_inr, funCongrLeft_apply, LinearMap.liftBaseChangeEquiv_symm_apply, Algebra.TensorProduct.equivFinsuppOfBasis_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl, AffineEquiv.map_vadd, Module.Basis.repr_linearCombination, TensorProduct.assoc_tmul, PiTensorProduct.reindex_tprod, Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply, LinearMap.prodEquiv_symm_apply, extendScalarsOfSurjective_apply, LinearIndependent.linearCombinationEquiv_apply_coe, TensorProduct.AlgebraTensorModule.leftComm_tmul, ModularGroup.lcRow0Extend_apply, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, cast_apply, StarModule.decomposeProdAdjoint_symm_apply, Module.Basis.dualBasis_equivFun, coe_toAddEquiv_symm, TensorProduct.congr_tmul, coe_toLexLinearEquiv, LinearMap.SeparatingRight.congr, symm_apply_apply, CharacterModule.intSpanEquivQuotAddOrderOf_apply, FiniteDimensional.basisSingleton_repr_apply, Subalgebra.linearEquivOp_apply_coe, Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero, TensorProduct.AlgebraTensorModule.assoc_tmul, coe_prodUnique, trans_apply, TensorProduct.AlgebraTensorModule.leftComm_symm_tmul, Finsupp.lsum_single, LinearMap.BilinForm.sum_repr_mul_repr_mul, Finsupp.linearEquivFunOnFinite_single, TensorProduct.AlgebraTensorModule.rightComm_tmul, Module.Basis.smulTower'_repr_mk, map_smulₛₗ, TensorProduct.AlgebraTensorModule.assoc_symm_tmul, TensorProduct.lid_symm_apply, IsTensorProduct.equiv_apply, TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, PiTensorProduct.liftEquiv_symm_apply, LocalizedModule.coe_map_eq, Module.Basis.equiv'_symm_apply, Module.Basis.repr_reindex, TensorProduct.lid_tmul, Module.subsingletonEquiv_symm_apply, extendScalarsOfIsLocalization_symm_apply, congrLeft_apply, Module.Basis.algebraMapCoeffs_repr_apply_toFun, piRing_symm_apply, TensorProduct.piRight_symm_apply, IsLocalizedModule.mapEquiv_apply, Submodule.span_image_linearEquiv, WithCStarModule.linearEquiv_apply, TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul, Module.Relations.Solution.IsPresentation.uniq_var, Module.Basis.algebraMapCoeffs_repr_apply_apply, ofInjective_apply, MultilinearMap.domDomCongrLinearEquiv_apply, PiTensorProduct.liftEquiv_apply, ofBijective_apply, ContinuousMultilinearMap.piLinearEquiv_apply, Complex.selfAdjointEquiv_apply, Submodule.comap_equiv_self_of_inj_of_le_apply, Rep.freeLiftLEquiv_apply, Submodule.set_smul_eq_map, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, AlgEquiv.coe_symm_toLinearEquiv, baseChange_tmul, Module.Basis.repr_symm_single, Submodule.quotEquivOfEqBot_apply_mk, ContinuousLinearMap.toSpanSingletonLE_apply, prodComm_apply, TensorProduct.prodRight_symm_tmul, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, conj_apply, DFinsupp.mapRange.linearEquiv_apply, ofSubmodules_symm_apply, Complex.equivRealProdLm_apply, LinearMap.kerComplementEquivRange_apply_coe, Submodule.restrictScalarsEquiv_symm_apply, Module.Basis.restrictScalars_repr_apply, Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp, Module.Basis.equivFunL_apply, Fintype.linearIndependent_iff'ₛ, TensorProduct.piRight_symm_single, FourierTransform.fourierEquiv_symm_apply, coe_toAffineEquiv, IsLocalizedModule.mapEquiv_symm_apply, Module.Basis.singleton_repr, TensorProduct.map_comm, toSpanNonzeroSingleton_apply, ContinuousLinearEquiv.coe_toLinearEquiv, DFinsupp.linearEquivFunOnFintype_symm_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, arrowCongr_apply, finTwoArrow_apply, Submodule.prodEquivOfIsCompl_symm_apply, skewProd_symm_apply, Submodule.Quotient.restrictScalarsEquiv_symm_mk, Matrix.liftLinear_apply, PiTensorProduct.lift_comp_reindex, PiTensorProduct.dualDistribEquivOfBasis_apply_apply, conjRingEquiv_apply_apply, Module.Basis.toDual_eq_repr, TensorProduct.lid'_apply_tmul, Rep.leftRegularHomEquiv_symm_apply, Module.Basis.sum_repr_mul_repr, symm_trans_apply, Module.Basis.linearMap_repr_apply, zero_apply, MultilinearMap.curryFinFinset_apply_const, LinearMap.lsum_single, LinearMap.nondegenerate_congr_iff, image_eq_preimage_symm, Module.dualProdDualEquivDual_apply_apply, Submodule.quotientPi_apply, ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply, LinearIsometryEquiv.withLpProdCongr_symm_apply, conj_symm_conj, coe_curry_symm, IsBaseChange.equiv_symm_apply, TensorProduct.congr_symm_tmul, Matrix.uniqueLinearEquiv_apply, Representation.ofMulActionSelfAsModuleEquiv_apply, exteriorPower.oneEquiv_symm_apply, piCongrLeft'_symm_apply, submoduleMap_apply, Module.Basis.mem_span_image, rTensor_symm_tmul, Module.Basis.localizationLocalization_repr_algebraMap, LinearMap.lTensor_comm, Module.Basis.dualBasis_apply, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, WithCStarModule.linearEquiv_symm_apply, Complex.equivRealProdLm_symm_apply_im, TensorProduct.tensorQuotientEquiv_apply_mk_tmul, Module.Basis.reindexFinsetRange_repr_self, symm_comp_eq, IsLocalizedModule.linearEquiv_symm_apply, LinearMap.equivProdOfSurjectiveOfIsCompl_apply, Module.Basis.repr_symm_single_one, LinearMap.BilinForm.congr_congr, Matrix.compLinearEquiv_symm_apply, Submodule.prodEquivOfIsCompl_symm_apply_left, Submodule.quotientEquivOfIsCompl_apply_mk_coe, uniqueProd_symm_apply, Matrix.toLinOfInv_symm_apply, alternatingMapCongrRight_apply_apply, Algebra.IsPushout.cancelBaseChangeAux_symm_tmul, LinearMap.isPairSelfAdjoint_equiv, LinearMap.quotKerEquivRange_symm_apply_image, Finsupp.lsum_apply, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, Submodule.Quotient.equiv_symm_apply, iSupIndep.linearEquiv_apply, Module.Basis.coe_finTwoProd_repr, PiTensorProduct.isEmptyEquiv_symm_apply, DistribMulAction.toLinearEquiv_apply, map_add, PiTensorProduct.subsingletonEquiv_symm_apply', Finsupp.coe_lsum, ContinuousLinearEquiv.coe_mk, TensorProduct.rid_tmul, CategoryTheory.Linear.homCongr_apply, CharacterModule.homEquiv_symm_apply_apply_apply, smulOfNeZero_apply, multilinearCurryLeftEquiv_apply, starL'_symm_apply, PiTensorProduct.tmulEquivDep_symm_apply, MultilinearMap.constLinearEquivOfIsEmpty_apply, finTwoArrow_symm_apply, MultilinearMap.curryFinFinset_symm_apply_const, coe_symm_mk, Finsupp.sigmaFinsuppLEquivPiFinsupp_apply, CategoryTheory.Iso.toLinearEquiv_apply, LinearIndependent.linearCombinationEquiv_symm_apply, Submodule.equivSubtypeMap_apply, Module.DualBases.basis_repr_apply, toLinearMap_eq_coe, DFinsupp.sigmaCurryLEquiv_symm_apply, LieModuleEquiv.coe_toLinearEquiv, Finsupp.llift_symm_apply, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, AffineMap.toConstProdLinearMap_apply, LinearMap.quotKerEquivRange_apply_mk, AddEquiv.coe_toLinearEquiv_symm, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply, Module.Basis.map_apply, Module.Basis.symmetricAlgebra_repr_apply, prodProdProdComm_apply, sumPiEquivProdPi_symm_apply, Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val, symmEquiv_apply_apply, MultilinearMap.domDomCongrLinearEquiv'_apply, PiTensorProduct.tmulEquivDep_apply, Polynomial.toFinsuppIsoLinear_apply, AlgEquiv.linearEquivConj_mulLeftRight, Module.Basis.constr_apply_fintype, symm_conj_apply, MultilinearMap.ofSubsingletonₗ_apply, DFinsupp.lsum_symm_apply, WithConv.linearEquiv_apply, AlgEquiv.coe_toLinearEquiv, conjAlgEquiv_apply_apply, algEquivOfRing_symm_apply, Submodule.quotientEquivOfIsCompl_symm_apply, Module.Relations.Solution.IsPresentation.uniq_symm_var, conj_conj_symm, ofSubsingleton_apply, coe_ofEq_apply, eq_comp_symm, AffineMap.toConstProdLinearMap_symm_apply, smul_apply, LocallyConstant.congrLeftₗ_symm_apply_apply, Matrix.toLin'OfInv_symm_apply, LinearMap.BilinForm.flip_apply, AffineEquiv.ofLinearEquiv_apply, IsLocalizedModule.iso_symm_apply_aux, TensorProduct.piScalarRight_symm_single, map_eq_zero_iff, Module.Basis.repr_apply_eq, ContinuousAlternatingMap.piLinearEquiv_symm_apply, prodUnique_symm_apply, TensorProduct.quotTensorEquivQuotSMul_symm_mk, AdicCompletion.of_ofLinearEquiv_symm, Submodule.quotientPi_symm_apply, LinearMap.BilinForm.comp_congr, LinearMap.kerComplementEquivRange_symm_apply, LinearMap.separatingLeft_congr_iff, Module.Basis.end_repr_symm_apply, LinearMap.GeneralLinearGroup.coe_ofLinearEquiv, Module.evalEquiv_apply, Complex.equivRealProdLm_symm_apply_re, Module.Basis.equiv'_apply, coord_self, Finsupp.lcongr_symm_single, Module.Basis.apply_eq_iff, sigmaFinsuppLequivDFinsupp_symm_apply, TensorProduct.leftComm_symm_tmul, ofLeftInverse_apply, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, RingEquiv.toSemilinearEquiv_symm_apply, coe_ofInvolutive, symmEquiv_symm_apply_apply, SemimoduleCat.Iso.conj_eq_conj, Module.Basis.coe_ofRepr, dualMap_apply, funUnique_apply, sumArrowLequivProdArrow_apply_fst, coe_zero, Finsupp.lcongr_single, submoduleMap_symm_apply, LinearMap.GeneralLinearGroup.coe_toLinearEquiv, Finsupp.linearEquivFunOnFinite_apply, Rep.coindVEquiv_apply_hom, toSpanNonzeroSingleton_symm_apply_smul, congrQuadraticMap_symm_apply, Module.Basis.dualBasis_repr, PiTensorProduct.tmulEquiv_apply, BialgEquiv.trans_symm_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr, prodCongr_apply, Module.Basis.linearCombination_repr, union_support_maximal_linearIndependent_eq_range_basis, MultilinearMap.curryMidLinearEquiv_apply, TensorProduct.quotientTensorEquiv_apply_tmul_mk, Pretrivialization.linearEquivAt_apply, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply, piCurry_symm_apply, Module.Basis.tensorAlgebra_repr_apply, symmEquiv_apply_symm_apply, TensorProduct.rightComm_tmul, LinearMap.coprodEquiv_apply, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, Module.Basis.equivFun_apply, Module.apply_evalEquiv_symm_apply, Module.Basis.smulTower'_repr, CliffordAlgebra.reverseEquiv_symm_apply, WithLp.linearEquiv_apply, ofSubmodule'_apply, Finsupp.LinearEquiv.finsuppUnique_apply, rTensor_trans_apply, Finsupp.linearEquivFunOnFinite_symm_single, TensorProduct.rid_symm_apply, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply, Submodule.mk_quotientEquivOfIsCompl_apply, Submodule.prodEquivOfIsCompl_symm_apply_right, Finsupp.mapRange.linearEquiv_apply, LocallyConstant.congrLeftₗ_apply_apply, SameRay.sameRay_map_iff, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply, ofTop_symm_apply, KaehlerDifferential.quotKerTotalEquiv_symm_apply, LinearMap.quotKerEquivOfSurjective_symm_apply, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul, smulOfNeZero_symm_apply, refl_apply, PiTensorProduct.lift_tprod, Matrix.toLinOfInv_apply, apply_symm_apply, Module.Invertible.rTensorEquiv_symm_apply_apply, Complex.selfAdjointEquiv_symm_apply, congr_arg, conj_id, DFinsupp.linearEquivFunOnFintype_apply, AddEquiv.coe_symm_toNatLinearEquiv, finsuppLequivDFinsupp_apply_apply, TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul, TensorProduct.lift.equiv_symm_apply, addMonoidHomLequivNat_apply, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, CategoryTheory.Linear.homCongr_symm_apply, Finsupp.domLCongr_apply, toFun_eq_coe, conjRingEquiv_symm_apply_apply, Finsupp.curryLinearEquiv_apply, TensorProduct.map_map_assoc, Matrix.uniqueLinearEquiv_symm_apply, sumArrowLequivProdArrow_apply_snd, Submodule.quotEquivOfEq_mk, RingEquiv.toSemilinearEquiv_apply, addMonoidHomLequivInt_symm_apply, congr_fun, Matrix.toLinearEquivRight'OfInv_apply, map_smul, smul_id_of_finrank_eq_one_apply, LinearMap.ringLmapEquivSelf_apply, PiTensorProduct.lift_comp_map, smul_def, Module.Basis.ext_elem_iff, AddEquiv.coe_toIntLinearEquiv, LinearMap.toContPerfPair_apply, multilinearCurryLeftEquiv_symm_apply, Module.Basis.repr_sum_self, piFinTwo_apply, Function.Exact.linearEquivOfSurjective_apply, MultilinearMap.coe_currySumEquiv, ofSubsingleton_symm_apply, Finsupp.supportedEquivFinsupp_symm_apply_coe, toSpanNonzeroSingleton_one, LinearMap.coe_quotientInfToSupQuotient, Module.Basis.smulTower_repr_mk, Module.Basis.repr_support_subset_of_mem_span, prodAssoc_apply, MultilinearMap.curryMidLinearEquiv_symm_apply, Finsupp.supportedEquivFinsupp_apply_support_val, finsuppLequivDFinsupp_symm_apply, Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply, Finsupp.lsum_comp_lsingle, CoalgEquiv.trans_symm_apply, TensorProduct.prodRight_tmul, Module.Basis.linearMap_repr_symm_apply, Module.Basis.constr_basis, IsBaseChange.equiv_tmul, ModuleCat.homLinearEquiv_apply, sumArrowLequivProdArrow_symm_apply_inl, ofIsUnitDet_apply, AlgEquiv.linearEquivConj_mulRight, ModuleCat.Iso.conj_eq_conj, CliffordAlgebra.reverseEquiv_apply, SemilinearEquivClass.semilinearEquiv_apply, Module.Ray.map_apply, TensorProduct.tensorTensorTensorAssoc_symm_tmul, coord_apply_smul, TensorProduct.lidOfCompatibleSMul_tmul, coe_toLinearMap, MulOpposite.coe_opLinearEquiv, Representation.coinvariantsFinsuppLEquiv_symm_apply, Subalgebra.linearEquivOp_symm_apply_coe, CategoryTheory.Abelian.Ext.mk₀_linearEquiv₀_apply, lTensor_trans_apply, ContinuousLinearMap.toSpanSingletonLE_symm_apply, AddEquiv.coe_toNatLinearEquiv, TensorProduct.lid'_symm_apply, PiTensorProduct.map_reindex, Rep.leftRegularHomEquiv_apply, ext_iff, Function.Exact.linearEquivOfSurjective_symm_apply, coe_injective, PiTensorProduct.lift.unique', TensorProduct.piScalarRight_apply, lTensor_symm_tmul, starLinearEquiv_apply, AlternatingMap.domDomCongrₗ_symm_apply, coe_one, coe_ofTop_symm_apply, TensorProduct.comm_tmul, Submodule.fstEquiv_symm_apply_coe, neg_apply, fromModuleCatToModuleCatLinearEquiv_apply, symm_smul_apply, fromModuleCatToModuleCatLinearEquiv_symm_apply_coe, PiTensorProduct.lift_comp_reindex_symm, coe_toEquiv_symm, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, Matrix.toLin'OfInv_apply, MultilinearMap.constLinearEquivOfIsEmpty_symm_apply, toWeakSpaceCLM_eq_toWeakSpace, Module.Basis.prod_repr_inr, pow_apply, symmEquiv_symm_apply_symm_apply, AlternatingMap.domLCongr_apply, Module.Basis.constr_self, toAddEquiv_toNatLinearEquiv, CategoryTheory.Abelian.Ext.linearEquiv₀_symm_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, injective, AdicCompletion.ofLinearEquiv_apply, ofIsUnitDet_symm_apply, Matrix.piLinearEquiv_symm_apply, LinearMap.extendScalarsOfIsLocalizationEquiv_symm_apply, Module.Basis.constr_def, Rep.freeLiftLEquiv_symm_apply, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply, ContinuousLinearMap.prodₗ_apply, ContinuousLinearMap.coprodEquiv_symm_apply, Module.Basis.toDual_apply_left, congrQuadraticMap_apply, Matrix.coe_ofLinearEquiv_symm, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply, LinearMap.coprodEquiv_symm_apply, map_mem_invtSubmodule_iff, LinearMap.mul'_comm, Module.Basis.reindexFinsetRange_repr, Module.Basis.smulTower_repr, Module.Basis.toDual_apply_right, AffineEquiv.map_vadd', AlternatingMap.domDomCongrₗ_apply, Rep.indResHomEquiv_apply_hom, Module.Basis.repr_symm_apply, Module.Dual.congr_apply_apply, Module.Basis.coe_ofEquivFun, ofLinear_symm_apply, coe_uniqueProd, alternatingMapCongrRight_symm_apply_apply, WithLp.linearEquiv_symm_apply, MultilinearMap.curryFinFinset_symm_apply, lTensor_refl_apply, Module.Basis.sum_equivFun, WithLp.coe_symm_linearEquiv, Submodule.comapSubtypeEquivOfLe_apply_coe, LinearMap.lsum_piSingle, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, Algebra.TensorProduct.equivPiOfFiniteBasis_apply, Module.Basis.constr_range, Module.Basis.repr_unitsSMul, Module.compHom.toLinearEquiv_symm_apply, TensorProduct.piRight_apply, arrowCongr_comp, Module.Basis.constr_apply, piCongrLeft'_apply, DFinsupp.lsum_apply_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, Derivation.linearEquiv_coe_comp, Finsupp.linearCombination_eq_fintype_linearCombination_apply, Matrix.compLinearEquiv_apply, instSemilinearEquivClass, ofInjective_symm_apply, AddEquiv.coe_toLinearEquiv, CharacterModule.homEquiv_apply_apply, Submodule.mem_map_equiv, TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk, coe_symm_mk', Module.Basis.repr_eq_iff', Submodule.map_equivMapOfInjective_symm_apply, Finsupp.supportedEquivFinsupp_symm_apply_coe_apply, SemimoduleCat.homLinearEquiv_symm_apply, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply, LieModule.shiftedGenWeightSpace.shift_symm_apply, Representation.linHom.invariantsEquivRepHom_apply_hom, Matrix.coe_ofLinearEquiv, Module.Basis.mem_span_repr_support, Finsupp.finsuppProdLEquiv_symm_apply_apply, Module.Basis.toDual_eq_equivFun, Module.Basis.sum_repr, Finsupp.supportedEquivFinsupp_apply_apply, TensorProduct.assoc_symm_tmul, CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom, TensorProduct.comm_symm_tmul, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, exteriorPower.zeroEquiv_symm_apply, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, PiTensorProduct.lift.unique, ContinuousAlternatingMap.piLinearEquiv_apply, Matrix.toLpLinAlgEquiv_symm_apply, Module.Basis.algebraMapCoeffs_repr, Submodule.sndEquiv_apply, multilinearMapCongrLeft_apply, LieEquiv.ofBijective_invFun, Submodule.sndEquiv_symm_apply_coe, Submodule.comapSubtypeEquivOfLe_symm_apply, Module.Basis.coord_apply, LinearMap.lsum_symm_apply, Module.Basis.mem_span_iff_repr_mem, KaehlerDifferential.quotKerTotalEquiv_apply, ULift.moduleEquiv_apply, Module.Basis.coord_equivFun_symm, Algebra.Generators.H1Cotangent.equiv_apply, rTensor_tmul, Submodule.Quotient.restrictScalarsEquiv_mk, Module.Basis.repr_self, IsLocalizedModule.lift_iso, Shrink.linearEquiv_apply, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply, Polynomial.taylorLinearEquiv_apply_coe, PiTensorProduct.congr_tprod, AdicCompletion.ofLinearEquiv_symm_of, ofTop_apply, Module.subsingletonEquiv_apply, Module.Basis.repr_reindex_apply, Matrix.transposeLinearEquiv_apply, LinearMap.quotKerEquivOfSurjective_apply_mk, coe_coe, Algebra.SubmersivePresentation.cotangentEquiv_apply, DirectSum.lequivProdDirectSum_symm_apply, TensorProduct.dualDistribEquivOfBasis_apply_apply, ofLinear_apply, Submodule.coe_equivMapOfInjective_apply, Module.dualProdDualEquivDual_symm_apply, Module.Basis.constr_eq, Fin.consLinearEquiv_symm_apply, Finsupp.domLCongr_single, apply_ofBijective_symm_apply, ContinuousLinearEquiv.coe_symm_toLinearEquiv, DirectSum.linearEquivFunOnFintype_apply, MultilinearMap.ofSubsingletonₗ_symm_apply, toAddEquiv_toIntLinearEquiv, coe_addEquiv_apply, TensorProduct.AlgebraTensorModule.congr_tmul, Submodule.piQuotientLift_mk, MultilinearMap.currySumEquiv_symm_apply, LinearMap.lflip_apply, TensorProduct.lift.equiv_apply, Rep.indResHomEquiv_symm_apply_hom, QuadraticForm.dualProdProdIsometry_invFun, LinearMap.SeparatingLeft.congr, Submodule.fstEquiv_apply, extendScalarsOfIsLocalization_apply, Finsupp.curryLinearEquiv_symm_apply, Module.Basis.coord_toDualEquiv_symm_apply, Finsupp.lsum_symm_apply, Module.Basis.coord_repr_symm, Finsupp.lcongr_apply_apply, StarModule.decomposeProdAdjoint_apply, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul, skewProd_apply, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, Ideal.isoBaseOfIsPrincipal_apply, prodUnique_apply, Module.Dual.congr_symm_apply_apply, Module.Basis.coe_sumCoords, Submodule.restrictScalarsEquiv_apply, coe_ofLexLinearEquiv, DirectSum.lequivProdDirectSum_apply, LinearMap.sum_repr_mul_repr_mul, Fin.consLinearEquiv_apply, IsLocalizedModule.iso_mk_one, Module.Basis.ofIsLocalizedModule_repr_apply, DFinsupp.domLCongr_apply, Submodule.Quotient.equiv_apply, conjAlgEquiv_ext_iff, TensorProduct.includeRight_lid, LieEquiv.coe_toLinearEquiv, TensorProduct.tensorTensorTensorAssoc_tmul, AddEquiv.coe_symm_toIntLinearEquiv, Module.compHom.toLinearEquiv_apply, IsNoetherian.equivPUnitOfProdInjective_symm_apply, Matrix.toLinearEquiv_apply, piRing_apply, PiTensorProduct.lift_symm, prodProdProdComm_toAddEquiv, sigmaFinsuppLequivDFinsupp_apply, AlgEquiv.toLinearEquiv_apply
instSMulUnitsId 📖	CompOp	10 math math: conjAlgEquiv_ext_iff', LinearIsometryEquiv.toLinearEquiv_smul, symm_smul, ContinuousLinearEquiv.toLinearEquiv_smul, smul_apply, toLinearMap_smul, trans_smul, symm_smul_apply, smul_trans, smul_refl
invFun 📖	CompOp	12 math math: right_inv, QuadraticMap.IsometryEquiv.prodProdProdComm_invFun, left_inv, invFun_eq_symm, QuadraticForm.dualProdIsometry_invFun, QuadraticMap.IsometryEquiv.prodComm_invFun, LinearMap.toMatrixOrthonormal_symm_apply, LieHom.quotKerEquivRange_invFun, ContinuousLinearEquiv.continuous_invFun, CategoryTheory.Iso.toIsometryEquiv_invFun, addMonoidEndRingEquivInt_symm_apply, QuadraticForm.dualProdProdIsometry_invFun
ofInvolutive 📖	CompOp	1 math math: coe_ofInvolutive
refl 📖	CompOp	75 math math: congrRight₂_refl, Finsupp.mapRange.linearEquiv_refl, AlternatingMap.domLCongr_refl, LinearMap.Nondegenerate.congr, AffineEquiv.linear_vaddConst, LinearMap.GeneralLinearGroup.congrLinearEquiv_refl, TensorProduct.AlgebraTensorModule.congr_refl, AddEquiv.toIntLinearEquiv_refl, Projectivization.map_id, domMulActCongrRight_symm_apply, DFinsupp.mapRange.linearEquiv_refl, AlternatingMap.domDomCongrₗ_refl, PiTensorProduct.reindex_refl, LinearMap.separatingRight_congr_iff, congrQuadraticMap_refl, domMulActCongrRight_apply, conj_refl, congrLeft_symm_apply, Module.Basis.equiv_refl, refl_mem_transvections, ModularGroup.lcRow0Extend_symm_apply, Module.Invertible.tensorProductComm_eq_refl, TensorProduct.congr_refl_refl, rTensor_refl_apply, TensorProduct.leftComm_def, refl_toLinearMap, ModularGroup.lcRow0Extend_apply, LinearMap.SeparatingRight.congr, Module.Ray.map_refl, refl_trans, AffineEquiv.linear_refl, withLpCongr_refl, congrLeft_apply, refl_symm, symm_trans_self, mapMatrix_refl, rTensor_refl, LinearMap.nondegenerate_congr_iff, refl_mem_dilatransvections, LinearMap.BilinForm.congr_refl, TensorProduct.comm_trans_comm, trans_refl, AffineEquiv.ofLinearEquiv_refl, AffineEquiv.linear_constVAdd, ofSubsingleton_self, LinearMap.separatingLeft_congr_iff, lTensor_refl, funCongrLeft_id, CoalgEquiv.refl_toLinearEquiv, TensorPower.cast_refl, AddEquiv.toNatLinearEquiv_refl, LinearMap.BilinForm.flip_flip, transvection.of_right_eq_zero, refl_apply, transvection.of_left_eq_zero, TensorProduct.tensorTensorTensorComm_trans_tensorTensorTensorComm, Finsupp.basisSingleOne_repr, SpecialLinearGroup.congr_linearEquiv_refl, Orientation.map_refl, Matrix.reindexLinearEquiv_refl_refl, IsLocalizedModule.iso_localizedModule_eq_refl, ofEq_rfl, Pi.basisFun_equivFun, dualMap_refl, one_eq_refl, lTensor_refl_apply, AlgEquiv.toLinearEquiv_refl, piCongrRight_refl, det_refl, smul_refl, self_trans_symm, Finsupp.domLCongr_refl, TensorProduct.rightComm_def, QuadraticForm.dualProdProdIsometry_invFun, LinearMap.SeparatingLeft.congr
symmEquiv 📖	CompOp	4 math math: symmEquiv_apply_apply, symmEquiv_symm_apply_apply, symmEquiv_apply_symm_apply, symmEquiv_symm_apply_symm_apply
toAddEquiv 📖	CompOp	15 math math: coe_toAddEquiv, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, Finsupp.mapRange.linearEquiv_toAddEquiv, DirectSum.congr_linearEquiv_toAddEquiv, WithLp.toAddEquiv_linearEquiv, QuadraticForm.dualProdIsometry_invFun, Representation.ofMulActionSelfAsModuleEquiv_apply, MulOpposite.opLinearEquiv_toAddEquiv, QuadraticForm.dualProdIsometry_toFun, map_dfinsuppSumAddHom, toAddMonoidHom_commutes, isScalarTower, DirectSum.congrLinearEquiv_toAddEquiv, MulOpposite.opLinearEquiv_symm_toAddEquiv, WithConv.toAddEquiv_linearEquiv
toEquiv 📖	CompOp	11 math math: coe_toEquiv, coe_symm_toEquiv, FirstOrder.Field.lift_genericMonicPoly, ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv, toEquiv_inj, toEquiv_symm, LinearIndependent.linearCombinationEquiv_symm_apply, toEquiv_injective, ContinuousLinearEquiv.coe_uniqueProd, ContinuousLinearEquiv.coe_prodUnique, coe_toEquiv_symm
toLinearMap 📖	CompOp	480 math math: Pi.comul_eq_adjoint, multilinearMapCongrLeft_symm_apply, LinearPMap.inverse_graph, SemimoduleCat.Hom.hom₂_apply, Module.Basis.det_comp_basis, Algebra.idealMap_eq_ofEq_comp_toLocalized₀, multilinearMapCongrRight_apply, Submodule.comap_equiv_eq_map_symm, GradedTensorProduct.hom_ext_iff, coe_toLinearMap_flip, coe_baseChange, RootPairing.Base.forall_mem_support_invtSubmodule_iff, LocalizedModule.restrictScalars_map_eq, LinearMap.exists_linearEquiv_eq_graph, LinearMap.lTensor_rTensor_comp_assoc, Submodule.mulMap_one_right_eq, skewAdjointLieSubalgebraEquiv_apply, Submodule.comap_op_mul, LieSubalgebra.mem_map_submodule, RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm, SpecialLinearGroup.toLinearEquiv_symm_to_linearMap, Algebra.Presentation.differentials.comm₂₃, QuotSMulTop.equivTensorQuot_naturality, SpecialLinearGroup.mem_center_iff_spec, TensorProduct.tensorTensorTensorComm_comp_map, instIsZLatticeComap, Submodule.comap_op_pow, symm_comp, CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap, Module.Dual.eval_comp_comp_evalEquiv_eq, map_mem_invtSubmodule_conj_iff, LinearMap.baseChange_baseChange, TensorPower.gMul_eq_coe_linearMap, TensorProduct.map_comp_comm_eq, Submodule.mem_invtSubmodule_reflection_of_mem, congrRight₂_apply, SpecialLinearGroup.mem_center_iff, right_inv, contractLeft_assoc_coevaluation, Module.Basis.ofZLatticeComap_apply, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, comp_toLinearMap_symm_eq, TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange, skewAdjointLieSubalgebraEquiv_symm_apply, LinearMap.mul'_comp_comm, comp_symm_cancel_left, toMatrix_rotation, Derivation.linearEquiv_coe_to_linearMap_comp, toLinearMap_inj, Submodule.dualCopairing_eq, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, range_comp, LinearMap.coe_equivProdOfSurjectiveOfIsCompl, RootPairing.Hom.weight_coweight_transpose, SemimoduleCat.hom_inv_rightUnitor, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, Orientation.map_eq_neg_iff_det_neg, toModuleIso_inv, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, coe_lTensor, Finsupp.linearCombination_smul, RootPairing.Equiv.weightHom_toLinearMap, TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor, conjAlgEquiv_apply, Submodule.mulMap_comm, mapMatrix_toLinearMap, TensorProduct.gradedMul_def, Finsupp.linearCombination_one_tmul, Pi.counit_eq_adjoint, LinearMap.trace_eq_contract_of_basis', QuadraticForm.tmul_comp_tensorComm, LinearMap.BilinForm.congr_comp, LinearMap.bijective_compr₂_of_equiv, AlgHom.toLinearMap_toOpposite, TensorProduct.toMatrix_assoc, LinearMap.lTensor_comp_comm, Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, coe_toLinearMap_mul, PiTensorProduct.reindex_comp_tprod, Pi.intrinsicStar_comul_commSemiring, Submodule.goursat, Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap, RootPairing.mem_invtRootSubmodule_iff, Orientation.det_rotation, Orientation.map_eq_iff_det_pos, TensorProduct.equivFinsuppOfBasisLeft_symm, Submodule.map_unop_mul, Submodule.coe_prodEquivOfIsCompl, Matrix.toLinearEquiv'_symm_apply, AffineEquiv.toAffineMap_mk, comp_toLinearMap_eq_iff, Polynomial.comap_taylorEquiv_degreeLT, lTensorHomEquivHomLTensor_toLinearMap, LinearMap.intrinsicStar_mul', mem_dilatransvections_iff_rank, IsLocalizedModule.iso_symm_comp, TensorProduct.AlgebraTensorModule.rTensor_tensor, RootPairing.corootSpan_map_flip_toPerfPair, det_symm_mul_det, LinearMap.IsPerfectCompl.isCompl_right, ZLattice.comap_equiv_apply, LinearMap.BilinForm.tensorDistribEquiv_toLinearMap, TensorProduct.directSumRight_comp_rTensor, SemimoduleCat.hom_hom_rightUnitor, Module.Invertible.bijective_curry, Module.Basis.repr_range, fst_comp_prodComm, LinearMap.rTensor_injective_iff_subtype, multilinearMapCongrRight_symm_apply, RootPairing.Equiv.coweightEquiv_one, Submodule.map_eq_top_iff, ofSubmodule'_symm_apply, left_inv, Module.Basis.repr_eq_iff, coe_toContinuousLinearEquiv_symm, LinearMap.IsPerfPair.compl₁₂, LinearMap.rTensor_lTensor_comp_assoc_symm, Submodule.map_orthogonal_equiv, Algebra.TensorProduct.equivFinsuppOfBasis_apply, conj_exact_iff_exact, TensorProduct.map_map_comp_assoc_eq, Algebra.TensorProduct.opAlgEquiv_apply, SpecialLinearGroup.det_eq_one, QuadraticForm.comp_tensorLId_eq, ModuleCat.hom_inv_associator, LinearMap.trace_eq_contract', exteriorPower.zeroEquiv_naturality, IsSymmetricAlgebra.equiv_symm_comp, refl_toLinearMap, Submodule.dualCoannihilator_map_linearEquiv_flip, RootPairing.rootSpan_map_toPerfPair, eq_toLinearMap_symm_comp, CoalgCat.MonoidalCategoryAux.tensorObj_comul, RootPairing.corootSpan_dualAnnihilator_map_eq, AffineEquiv.linear_toAffineMap, LinearMap.isSymmetric_linearIsometryEquiv_conj_iff, DirectSum.coe_congr_linearEquiv, comp_symm_assoc, Submodule.coe_quotEquivOfEqBot_symm, Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl, LieDerivation.exp_apply, Function.Exact.split_tfae, AdicCompletion.coe_ofTensorProductEquivOfFiniteNoetherian, Submodule.map_unop_pow, Submodule.orderIsoMapComap_apply', exteriorPower.oneEquiv_naturality, instIsPerfPair, comp_symm, Module.reflection_mul_reflection_pow, SemimoduleCat.hom_inv_leftUnitor, toLinearMap_injective, DirectSum.congr_linearEquiv_toLinearMap, symm_comp_cancel_right, extendOfIsometry_symm_apply, IsLocalizedModule.mapEquiv_apply, Submodule.span_image_linearEquiv, Polynomial.det_taylorLinearEquiv_toLinearMap, Matrix.toLin'_reindex, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, ModuleCat.hom_hom_leftUnitor, symm_comp_assoc, mem_dilatransvections_iff_finrank, ModuleCat.hom_hom_rightUnitor, eq_comp_toLinearMap_symm, LinearMap.comm_comp_lTensor_comp_comm_eq, conj_apply, toLinearMap_symm_comp_eq, isPositive_symm_iff, Coalgebra.IsCocomm.comm_comp_comul, Algebra.Generators.snd_comp_cotangentCompLocalizationAwayEquiv, DirectSum.congrLinearEquiv_toLinearMap, Submodule.equivOpposite_apply, MvPolynomial.rTensorAlgHom_toLinearMap, Rep.finsuppTensorRight_hom_hom, QuotSMulTop.equivQuotTensor_naturality, IsLocalizedModule.mapEquiv_symm_apply, Module.symm_dualMap_evalEquiv, BialgEquiv.toLinearMap_ofAlgEquiv, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, LinearMap.isPositive_linearIsometryEquiv_conj_iff, MulOpposite.counit_def, Module.Presentation.ofLinearEquiv_toSolution, MulOpposite.coe_opLinearEquiv_toLinearMap, Submodule.map_op_pow, RootPairing.corootSpan_mem_invtSubmodule_coreflection, CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap, Algebra.Presentation.differentials.comm₂₃', PiTensorProduct.lift_comp_reindex, IsLocalizedModule.lift_comp_iso, Submodule.starProjection_map_apply, AffineEquiv.coe_linear, SemimoduleCat.hom_inv_associator, addMonoidEndRingEquivInt_apply, Module.Basis.det_map', isUnit_det', Submodule.mulRightMap_eq_mulMap_comp, LinearMap.surjective_compr₂_of_equiv, Module.Basis.orientation_comp_linearEquiv_eq_iff_det_pos, ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, extendOfIsometry_apply, ker_comp, Submodule.orderIsoMapComap_symm_apply', Rep.ofMulActionSubsingletonIsoTrivial_inv_hom, Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg, submoduleMap_apply, extend_symm_apply, Rep.diagonalOneIsoLeftRegular_inv_hom, ModuleCat.hom_inv_rightUnitor, snd_comp_prodComm, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, Finsupp.mapRange.linearEquiv_toLinearMap, ZSpan.map, LinearMap.rTensor_comp_comm, Submodule.map_equiv_eq_comap_symm, LinearMap.isPairSelfAdjoint_equiv, Rep.coindIso_inv_hom_hom, eq_comp_toLinearMap_iff, Coalgebra.coassoc, snd_comp_prodAssoc, TensorProduct.toLinearMap_congr, comp_symm_cancel_right, Submodule.orderIsoMapComap_symm_apply, LinearMap.toMatrixOrthonormal_apply, Submodule.toLinearMap_prodEquivOfIsCompl_symm, toModuleIsoₛ_hom, coe_ofIsUnitDet, toLinearMap_eq_coe, comp_coe, Submodule.map_eq_bot_iff, Submodule.reflection_map, Submodule.det_reflection, toModuleIsoₛ_inv, Algebra.TensorProduct.opAlgEquiv_symm_apply, Submodule.orderIsoMapComap_apply, symmEquiv_apply_apply, Function.Exact.split_tfae', RootPairing.reflection_dualMap_eq_coreflection, symm_conj_apply, LinearMap.coe_equivOfIsUnitDet, AdicCompletion.congr_symm_apply, homTensorHomEquiv_toLinearMap, SpecialLinearGroup.centerEquivRootsOfUnity_apply, Rep.ofMulActionSubsingletonIsoTrivial_hom_hom, Orientation.rotation_eq_matrix_toLin, Finsupp.linearCombination_restrict, Algebra.Presentation.differentials.comm₁₂, Submodule.map_symm_eq_iff, Submodule.map_op_mul, RootPairing.ker_rootForm_eq_dualAnnihilator, ofSubmodule'_toLinearMap, DirectSum.decomposeLinearEquiv_symm_comp_lof, ofInjectiveEndo_right_inv, toLinearMap_smul, Ideal.constr_basisSpanSingleton, isUnit_det, Submodule.mulMap_one_left_eq, Matrix.toLinearEquiv'_apply, LinearIsometryEquiv.submoduleMap_symm_apply_coe, LinearMap.BilinForm.comp_congr, Submodule.mulMap_comm_of_commute, CoalgEquiv.toLinearEquiv_toLinearMap, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, ModuleCat.hom_hom_associator, Pretrivialization.linearMapAt_def_of_mem, RootPairing.polarizationEquiv_toLinearMap, Rep.finsuppTensorRight_inv_hom, AlgEquiv.toLinearEquiv_toLinearMap, isSymmetric_symm_iff, coe_toContinuousLinearEquiv, symmEquiv_symm_apply_apply, WithCStarModule.map_top_submodule, Finsupp.linearCombination_comp_addSingleEquiv, QuadraticForm.comp_tensorRId_eq, AlgHom.toLinearMap_fromOpposite, AdicCompletion.tensor_map_id_left_eq_map, Module.End.mem_invtSubmodule_symm_iff_le_map, CharacterModule.dual_rTensor_conj_homEquiv, CoalgEquiv.symm_toCoalgHom, Submodule.mulLeftMap_eq_mulMap_comp, TensorProduct.counit_def, PointedCone.minTensorProduct_comm, Module.Basis.det_basis, LinearMap.IsProj.eq_conj_prod_map', submoduleMap_symm_apply, rTensorHomEquivHomRTensor_toLinearMap, IsBaseChange.ofEquiv, congrQuadraticMap_symm_apply, RootPairing.Equiv.weightEquiv_one, MultilinearMap.comp_linearEquiv_eq_zero_iff, PiTensorProduct.map_comp_reindex_symm, Subspace.dualEquivDual_def, coe_rTensor_symm, SemimoduleCat.hom_hom_associator, Submodule.map_unop_one, dualTensorHomEquivOfBasis_toLinearMap, Submodule.reflection_map_apply, Matrix.SpecialLinearGroup.toLin'_to_linearMap, Module.Basis.coe_repr_symm, toAddMonoidHom_commutes, SemimoduleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, Rep.finsuppTensorLeft_inv_hom, ofSubmodule'_apply, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, Rep.leftRegularTensorTrivialIsoFree_inv_hom, transvection.coe_toLinearMap, Ideal.pi_mkQ_rTensor, toFGModuleCatIso_hom, TensorProduct.comul_def, Trivialization.linearMapAt_def_of_mem, det_mul_det_symm, Module.fgSystem.equiv_comp_of, ModuleCat.uliftFunctor_map, Rep.linearization_δ_hom, Matrix.toPerfectPairing, LinearMap.surjective_compr₂ₛₗ_of_equiv, toFun_eq_coe, Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap, PointedCone.maxTensorProduct_comm, RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root', rank_map_eq, Module.Relations.Solution.IsPresentation.of_linearEquiv, LinearMap.det_conj, instDiscreteTopologySubtypeMemSubmoduleIntComap, ModuleCat.Hom.hom₂_apply, TensorProduct.toLinearMap_symm_lid, Rep.finsuppTensorLeft_hom_hom, RootPairing.toPerfPair_conj_reflection, Finsupp.linearCombination_eq_fintype_linearCombination, coe_lTensor_symm, Module.Basis.parallelepiped_map, Module.Relations.Solution.IsPresentation.postcomp_uniq, coe_ofInjectiveOfFinrankEq, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, Submodule.comap_unop_pow, Algebra.tensorH1CotangentOfIsLocalization_toLinearMap, MeasureTheory.Measure.addHaar_preimage_linearEquiv, RootPairing.rootSpan_mem_invtSubmodule_reflection, Algebra.Extension.H1Cotangent.equivOfFormallySmooth_toLinearMap, ZLattice.covolume_comap, Module.Basis.ofZLatticeBasis_comap, coe_inv_det, RootPairing.toPerfPair_flip_conj_coreflection, Module.Relations.Solution.IsPresentation.postcomp_uniq_symm, QuadraticMap.IsometryEquiv.map_app', coe_toLinearMap, TensorProduct.equivFinsuppOfBasisRight_symm, MulOpposite.comul_def, Coalgebra.coassoc_symm, Rep.diagonalOneIsoLeftRegular_hom_hom, Finsupp.mapDomain.toLinearMap_linearEquiv, det_rotation, fst_comp_prodAssoc, ofInjectiveEndo_left_inv, LinearMap.rid_comp_lTensor, SpecialLinearGroup.coe_toGeneralLinearGroup_apply, ModuleCat.hom_inv_leftUnitor, Matrix.mulVecLin_reindex, Module.Basis.ofZLatticeComap_repr_apply, Algebra.Generators.H1Cotangent.δ_comp_equiv, Orientation.map_apply, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm, arrowCongrAddEquiv_apply, Submodule.map_range_rTensor_subtype_lid, Rep.freeLift_hom, LinearMap.mul'_tensor, extend_apply, det_coe_symm, Projectivization.generalLinearGroup_smul_def, PiTensorProduct.lift_comp_reindex_symm, Submodule.equivOpposite_symm_apply, LinearMap.bijective_compr₂ₛₗ_of_equiv, TensorProduct.map_map_comp_assoc_symm_eq, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, RootPairing.rootSpan_dualAnnihilator_map_eq, RootPairing.Equiv.inv_coweightMap, AlternatingMap.domLCongr_apply, TensorProduct.comm_comp_comm_assoc, LinearMap.toMatrix_basis_equiv, TensorProduct.comm_comp_comm, Submodule.comap_unop_one, Module.evalEquiv_toLinearMap, ofLinear_toLinearMap, SemimoduleCat.hom_hom_leftUnitor, coe_prodCongr, PiTensorProduct.map_comp_reindex_eq, LinearMap.lid_comp_rTensor, Submodule.mulMap_op, IsTensorProduct.equiv_toLinearMap, Module.Basis.constr_def, finrank_map_eq, AdicCompletion.congr_apply, congrQuadraticMap_apply, TensorProduct.lift_comp_comm_eq, AffineBasis.coord_smul, lift_rank_map_eq, arrowCongrAddEquiv_symm_apply, map_mem_invtSubmodule_iff, coe_trans, Submodule.goursat_surjective, MulOpposite.coe_opLinearEquiv_symm_toLinearMap, Submodule.dualAnnihilator_map_linearEquiv_flip_symm, ContinuousLinearEquiv.continuous_toFun, LinearMap.transvection.congr, IsLocalizedModule.of_linearEquiv, TensorProduct.quotTensorEquivQuotSMul_comp_mk, Submodule.HasOrthogonalProjection.map_linearIsometryEquiv, automorphismGroup.toLinearMapMonoidHom_apply, QuadraticForm.tmul_comp_tensorAssoc, Module.Invertible.rightCancelEquiv_comp_rTensor_comp_symm, ker, IsLocalizedModule.map_iso_commute, Submodule.comap_op_one, Algebra.TensorProduct.equivPiOfFiniteBasis_apply, entryLinearMap_comp_mapMatrix, Submodule.map_op_one, Submodule.map_dualCoannihilator_linearEquiv_flip, Submodule.exists_equiv_eq_graph, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, TensorProduct.toLinearMap_symm_rid, CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap, Derivation.linearEquiv_coe_comp, LieAlgebra.Extension.twoCocycleOf_coe_coe, Submodule.mem_map_equiv, RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', RootPairing.coroot'_reflectionPerm, ofLinear_symm_toLinearMap, TensorProduct.toMatrix_comm, RootPairing.Equiv.coweightHom_toLinearMap, Polynomial.coe_taylorEquiv, ModuleCat.monoidalClosed_pre_app, trans_dualMap_symm_flip, toModuleIso_hom, LinearMap.comm_comp_rTensor_comp_comm_eq, multilinearMapCongrLeft_apply, LinearMap.lTensor_tensor, toFGModuleCatIso_inv, RootPairing.ker_corootForm_eq_dualAnnihilator, Coalgebra.comm_comp_comul, Rep.coindIso_hom_hom_hom, Rep.leftRegularTensorTrivialIsoFree_hom_hom, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, Algebra.Generators.CotangentSpace.fst_compEquiv, Matrix.entryLinearMap_eq_comp, Submodule.mem_invtSubmodule_reflection_iff, LinearMap.associated_det_comp_equiv, LinearMap.IsPerfectCompl.isCompl_left, symm_comp_cancel_left, Submodule.map_dualAnnihilator_linearEquiv_flip_symm, CategoryTheory.Iso.toLinearMap_toLinearEquiv, AlternatingMap.compLinearEquiv_eq_zero_iff, coe_toLinearMap_one, Module.reflection_mul_reflection_zpow, Complex.det_conjLIE, LinearMap.intrinsicStar_eq_comp, coe_coe, contractLeft_assoc_coevaluation', ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, SpecialLinearGroup.toLinearEquiv_to_linearMap, Submodule.comap_unop_mul, lsum_comp_mapRange_toSpanSingleton, range, coe_rTensor, ModuleCat.ihom_ev_app, Subspace.dualPairing_eq, TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm, RootPairing.Equiv.inv_weightMap, coe_det, IsLocalizedModule.of_linearEquiv_right, Module.Invertible.leftCancelEquiv_comp_lTensor_comp_symm, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, DirectSum.coe_congrLinearEquiv, LinearMap.rTensor_tensor, Polynomial.map_taylorEquiv_degreeLT, Rep.linearization_μ_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, LinearIsometryEquiv.submoduleMap_apply_coe
trans 📖	CompOp	116 math math: Module.Basis.map_equivFun, Matrix.reindexLinearEquiv_trans, Submodule.comm_trans_lTensorOne, Submodule.toLinearEquiv_orthogonalDecomposition_symm, TensorProduct.congr_congr, det_trans, Submodule.toLinearEquiv_orthogonalDecomposition, RootPairing.Equiv.coweightEquiv_comp_toLin, conj_trans, TensorPower.cast_trans, piCongrRight_trans, dualMap_trans, DFinsupp.mapRange.linearEquiv_trans, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, AffineSubspace.linear_topEquiv, AddEquiv.toIntLinearEquiv_trans, Module.Basis.map_repr, Module.Basis.equiv_trans, comm_trans_lTensor_trans_comm_eq, mul_eq_trans, TensorProduct.comm_trans_lid, Module.Basis.coe_toOrthonormalBasis_repr, rTensor_trans_congr, Module.Basis.repr_smul, lTensor_trans_congr, TensorProduct.congr_trans, Finsupp.domLCongr_trans, LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr, PiTensorProduct.reindex_trans, Matrix.toPerfectPairing_apply_apply, SpecialLinearGroup.congr_linearEquiv_coe_apply, TensorProduct.leftComm_def, symm_flip, ContinuousLinearEquiv.trans_toLinearEquiv, Module.Basis.coe_toOrthonormalBasis_repr_symm, trans_apply, refl_trans, RootPairing.Equiv.weightEquiv_mul, Submodule.comm_trans_rTensorOne, symm_trans_self, Module.reflection_reflection_iterate, AddEquiv.toNatLinearEquiv_trans, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, congr_trans_rTensor, Module.infinite_range_reflection_reflection_iterate_iff, RootPairing.Equiv.coweightEquiv_mul, symm_trans_apply, Submodule.prodComm_trans_prodEquivOfIsCompl, LinearMap.GeneralLinearGroup.congrLinearEquiv_apply, Matrix.l2_opNNNorm_def, det_conj, LinearMap.BilinForm.congr_congr, Equiv.tensorProductAssoc_def, TensorProduct.comm_trans_comm, mapMatrix_trans, comp_coe, trans_refl, Trivialization.coordChangeL_symm_apply, AffineEquiv.ofLinearEquiv_trans_ofLinearEquiv, TensorProduct.assoc_tensor'', Trivialization.coe_coordChangeL', AffineSubspace.linear_equivMapOfInjective, symm_trans_cancel_right, trans_symm_cancel_left, Module.Basis.mulOpposite_repr_eq, LinearMap.BilinForm.flip_flip, rTensor_trans_apply, transvection.trans_of_left_eq, Rep.leftRegularTensorTrivialIsoFree_inv_hom, trans_smul, Matrix.toPerfectPairing, congrRight₂_trans, TensorProduct.tensorTensorTensorComm_trans_tensorTensorTensorComm, CoalgEquiv.trans_toLinearEquiv, comm_trans_rTensor_trans_comm_eq, Trivialization.coe_coordChangeL, transvection.trans_of_right_eq, OrthonormalBasis.coe_toBasis_repr, LinearMap.GeneralLinearGroup.congrLinearEquiv_trans', lTensor_trans_apply, RootPairing.Equiv.weightEquiv_comp_toLin, LinearMap.BilinForm.congr_trans, Finsupp.mapRange.linearEquiv_trans, Module.Basis.mapCoeffs_repr, trans_symm, LinearMap.GeneralLinearGroup.congrLinearEquiv_trans, arrowCongr_trans, symm_trans_cancel_left, AlternatingMap.domLCongr_trans, rTensor_trans_lTensor, Submodule.mulMap_op, smul_trans, TensorProduct.AlgebraTensorModule.congr_trans, coe_trans, TensorProduct.assoc_tensor, rTensor_trans, Equiv.tensorProductComm_def, TensorProduct.assoc_tensor', lTensor_trans_rTensor, withLpCongr_trans, Matrix.l2_opNorm_def, trans_assoc, funCongrLeft_comp, SpecialLinearGroup.congr_linearEquiv_trans, trans_dualMap_symm_flip, AlgEquiv.toLinearEquiv_trans, self_trans_symm, Rep.leftRegularTensorTrivialIsoFree_hom_hom, trans_symm_cancel_right, TensorProduct.rightComm_def, lTensor_trans, TensorProduct.comm_trans_rid, TensorProduct.lid_tensor, congr_trans_lTensor, baseChange_trans, LinearIsometryEquiv.toLinearEquiv_trans
transNotation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	right_inv
bijective 📖	mathematical	—	Function.Bijective DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	Equiv.bijective
cast_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike cast	—	RingHomInvPair.ids
cast_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike symm cast	—	RingHomInvPair.ids
coe_addEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquivClass.toAddEquiv LinearEquiv instEquivLike SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass	—	SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass
coe_coe 📖	mathematical	—	DFunLike.coe LinearMap LinearMap.instFunLike toLinearMap LinearEquiv EquivLike.toFunLike instEquivLike	—	—
coe_injective 📖	mathematical	—	LinearEquiv DFunLike.coe EquivLike.toFunLike instEquivLike	—	DFunLike.coe_injective
coe_mk 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike LinearMap LinearMap.instFunLike	—	—
coe_ofInvolutive 📖	mathematical	Function.Involutive DFunLike.coe LinearMap LinearMap.instFunLike	LinearEquiv EquivLike.toFunLike instEquivLike ofInvolutive	—	—
coe_symm_mk 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddHom.toFun 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 RingHom.id LinearMap.toAddHom	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike instEquivLike symm	—	RingHomInvPair.ids
coe_symm_mk' 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom RingHom.id Semiring.toNonAssocSemiring	DFunLike.coe LinearEquiv RingHomInvPair.ids EquivLike.toFunLike instEquivLike symm	—	RingHomInvPair.ids
coe_symm_toEquiv 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toEquiv LinearEquiv instEquivLike symm	—	—
coe_toAddEquiv 📖	mathematical	—	toAddEquiv AddEquivClass.toAddEquiv LinearEquiv instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass	—	—
coe_toAddEquiv_symm 📖	mathematical	—	AddEquivClass.toAddEquiv LinearEquiv instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass symm AddEquiv.symm	—	SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass
coe_toEquiv 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toEquiv LinearEquiv instEquivLike	—	—
coe_toEquiv_symm 📖	mathematical	—	Equiv.symm toEquiv EquivLike.toEquiv LinearEquiv instEquivLike symm	—	—
coe_toLinearMap 📖	mathematical	—	DFunLike.coe LinearMap LinearMap.instFunLike toLinearMap LinearEquiv EquivLike.toFunLike instEquivLike	—	—
coe_trans 📖	mathematical	—	toLinearMap trans LinearMap.comp	—	—
comp_coe 📖	mathematical	—	LinearMap.comp toLinearMap trans	—	—
comp_symm 📖	mathematical	—	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ toLinearMap symm LinearMap.id	—	LinearMap.ext RingHomInvPair.triples₂ apply_symm_apply
comp_symm_assoc 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext apply_symm_apply
comp_symm_cancel_left 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext comp_symm_assoc
comp_symm_cancel_right 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext apply_symm_apply
comp_symm_eq 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.comp_symm_eq
comp_toLinearMap_eq_iff 📖	mathematical	—	LinearMap.comp toLinearMap	—	toLinearMap_symm_comp_eq eq_toLinearMap_symm_comp
comp_toLinearMap_symm_eq 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext LinearMap.comp.congr_simp symm_apply_apply apply_symm_apply
congr_arg 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	DFunLike.congr_arg
congr_fun 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	DFunLike.congr_fun
eq_comp_symm 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_comp_symm
eq_comp_toLinearMap_iff 📖	mathematical	—	LinearMap.comp toLinearMap	—	eq_comp_toLinearMap_symm
eq_comp_toLinearMap_symm 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext LinearMap.comp.congr_simp symm_apply_apply apply_symm_apply
eq_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_symm_apply
eq_symm_comp 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_symm_comp
eq_toLinearMap_symm_comp 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext LinearMap.comp.congr_simp comp_symm_assoc symm_comp_assoc
ext 📖	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	ext
image_eq_preimage_symm 📖	mathematical	—	Set.image DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike Set.preimage symm	—	Equiv.image_eq_preimage_symm
image_symm_eq_preimage 📖	mathematical	—	Set.image DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm Set.preimage	—	Equiv.image_eq_preimage_symm
injective 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	Equiv.injective
instSemilinearEquivClass 📖	mathematical	—	SemilinearEquivClass LinearEquiv instEquivLike	—	AddHom.map_add' LinearMap.map_smul'
invFun_eq_symm 📖	mathematical	—	invFun DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	—
left_inv 📖	mathematical	—	invFun AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom toLinearMap	—	—
map_add 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass instSemilinearEquivClass
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	AddEquiv.map_eq_zero_iff
map_ne_zero_iff 📖	—	—	—	—	AddEquiv.map_ne_zero_iff
map_smul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass instSemilinearEquivClass
map_smulₛₗ 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike 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	—	LinearMap.map_smul'
map_zero 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass instSemilinearEquivClass
mk_coe 📖	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom toLinearMap	—	—	ext
mk_coe' 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddHom.toFun 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 LinearEquiv EquivLike.toFunLike instEquivLike LinearMap.toAddHom	symm	—	Function.Bijective.injective symm_bijective ext
refl_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike refl	—	RingHomInvPair.ids
refl_symm 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids refl	—	RingHomInvPair.ids
refl_toLinearMap 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids refl LinearMap.id	—	RingHomInvPair.ids
refl_trans 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomCompTriple.right_ids RingHomInvPair.ids refl	—	toEquiv_injective RingHomCompTriple.ids RingHomCompTriple.right_ids RingHomInvPair.ids Equiv.refl_trans
right_inv 📖	mathematical	—	invFun AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom toLinearMap	—	—
self_trans_symm 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ RingHomInvPair.ids symm refl	—	ext RingHomInvPair.ids RingHomInvPair.triples₂ symm_apply_apply
smul_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSMulUnitsId SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Units.val	—	RingHomInvPair.ids
smul_trans 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearEquiv instSMulUnitsId	—	RingHomInvPair.ids ext RingHomCompTriple.ids LinearMapClass.map_smul_of_tower SemilinearEquivClass.instSemilinearMapClass instSemilinearEquivClass LinearMap.IsScalarTower.compatibleSMul
surjective 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	Equiv.surjective
symmEquiv_apply_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike Equiv Equiv.instEquivLike symmEquiv LinearMap LinearMap.instFunLike LinearMap.inverse toLinearMap symm left_inv right_inv	—	—
symmEquiv_apply_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm Equiv Equiv.instEquivLike symmEquiv	—	—
symmEquiv_symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike Equiv Equiv.instEquivLike Equiv.symm symmEquiv LinearMap LinearMap.instFunLike LinearMap.inverse toLinearMap symm left_inv right_inv	—	—
symmEquiv_symm_apply_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm Equiv Equiv.instEquivLike Equiv.symm symmEquiv	—	—
symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	left_inv
symm_apply_eq 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_apply_eq
symm_bijective 📖	mathematical	—	Function.Bijective LinearEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_comp 📖	mathematical	—	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ toLinearMap symm LinearMap.id	—	LinearMap.ext RingHomInvPair.triples₂ symm_apply_apply
symm_comp_assoc 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext symm_apply_apply
symm_comp_cancel_left 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext symm_comp_assoc
symm_comp_cancel_right 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext symm_apply_apply
symm_comp_eq 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_comp_eq
symm_mk 📖	mathematical	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddHom.toFun 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 LinearMap.toAddHom	symm	—	—
symm_smul 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearEquiv instSMulUnitsId Units.instInv	—	RingHomInvPair.ids
symm_smul_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike symm Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSMulUnitsId SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Units.val Units.instInv	—	RingHomInvPair.ids
symm_symm 📖	mathematical	—	symm	—	—
symm_trans_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm trans	—	—
symm_trans_cancel_left 📖	mathematical	—	trans symm	—	ext apply_symm_apply
symm_trans_cancel_right 📖	mathematical	—	trans symm	—	ext apply_symm_apply
symm_trans_self 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ RingHomInvPair.ids symm refl	—	ext RingHomInvPair.ids RingHomInvPair.triples₂ apply_symm_apply
toAddMonoidHom_commutes 📖	mathematical	—	LinearMap.toAddMonoidHom toLinearMap AddEquiv.toAddMonoidHom AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid toAddEquiv	—	—
toEquiv_inj 📖	mathematical	—	toEquiv	—	toEquiv_injective
toEquiv_injective 📖	mathematical	—	LinearEquiv Equiv toEquiv	—	LinearMap.ext left_inv right_inv
toEquiv_symm 📖	mathematical	—	toEquiv symm Equiv.symm	—	—
toFun_eq_coe 📖	mathematical	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom toLinearMap DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	—
toLinearMap_eq_coe 📖	mathematical	—	toLinearMap SemilinearMapClass.semilinearMap LinearEquiv EquivLike.toFunLike instEquivLike SemilinearEquivClass.instSemilinearMapClass instSemilinearEquivClass	—	—
toLinearMap_inj 📖	mathematical	—	toLinearMap	—	toLinearMap_injective
toLinearMap_injective 📖	mathematical	—	LinearEquiv LinearMap toLinearMap	—	toEquiv_injective Equiv.ext LinearMap.congr_fun
toLinearMap_smul 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearEquiv instSMulUnitsId LinearMap LinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid Module.toDistribMulAction Units.val	—	RingHomInvPair.ids
toLinearMap_symm_comp_eq 📖	mathematical	—	LinearMap.comp toLinearMap symm	—	LinearMap.ext LinearMap.comp.congr_simp comp_symm_assoc symm_comp_assoc
trans_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike trans	—	—
trans_assoc 📖	mathematical	—	trans	—	—
trans_refl 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.right_ids RingHomCompTriple.ids RingHomInvPair.ids refl	—	toEquiv_injective RingHomCompTriple.right_ids RingHomCompTriple.ids RingHomInvPair.ids Equiv.trans_refl
trans_smul 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearEquiv instSMulUnitsId	—	RingHomInvPair.ids ext RingHomCompTriple.ids
trans_symm 📖	mathematical	—	symm trans	—	—
trans_symm_cancel_left 📖	mathematical	—	trans symm	—	ext symm_apply_apply
trans_symm_cancel_right 📖	mathematical	—	trans symm	—	ext symm_apply_apply

LinearEquiv.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—
symm_apply 📖	CompOp	—

LinearEquiv.symm_mk

Definitions

Name	Category	Theorems
aux 📖	CompOp	—

RingEquiv

Definitions

Name	Category	Theorems
toSemilinearEquiv 📖	CompOp	2 math math: toSemilinearEquiv_symm_apply, toSemilinearEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSemilinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass symm RingHomInvPair.of_ringEquiv RingHomInvPair.symm NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearEquiv.instEquivLike toSemilinearEquiv	—	RingEquivClass.toRingHomClass instRingEquivClass RingHomInvPair.of_ringEquiv RingHomInvPair.symm
toSemilinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass symm RingHomInvPair.symm RingHomInvPair.of_ringEquiv NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearEquiv.instEquivLike LinearEquiv.symm toSemilinearEquiv Equiv.invFun toEquiv	—	RingEquivClass.toRingHomClass instRingEquivClass RingHomInvPair.symm RingHomInvPair.of_ringEquiv

SemilinearEquivClass

Definitions

Name	Category	Theorems
instCoeToSemilinearEquiv 📖	CompOp	—
semilinearEquiv 📖	CompOp	22 math math: Polynomial.comap_taylorEquiv_degreeLT, CoalgEquiv.coe_toLinearEquiv, IsSymmetricAlgebra.equiv_symm_comp, Algebra.TensorProduct.leftComm_toLinearEquiv, BialgEquiv.toLinearMap_ofAlgEquiv, CoalgEquiv.toLinearEquiv_toLinearMap, CoalgEquiv.symm_toLinearEquiv, CoalgEquiv.symm_toCoalgHom, CoalgEquiv.refl_toLinearEquiv, CoalgEquiv.coe_symm_toLinearEquiv, BialgEquiv.trans_symm_apply, Coalgebra.TensorProduct.lid_toLinearEquiv, CoalgEquiv.trans_toLinearEquiv, CoalgEquiv.trans_symm_apply, semilinearEquiv_apply, Coalgebra.TensorProduct.rid_toLinearEquiv, CoalgEquiv.toLinearEquiv_eq_coe, Coalgebra.TensorProduct.assoc_toLinearEquiv, TensorProduct.congrIsometry_apply, Polynomial.coe_taylorEquiv, Polynomial.taylorLinearEquiv_apply_coe, Polynomial.map_taylorEquiv_degreeLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSemilinearMapClass 📖	mathematical	—	SemilinearMapClass EquivLike.toFunLike	—	AddEquivClass.map_add toAddEquivClass map_smulₛₗ
map_smulₛₗ 📖	mathematical	—	DFunLike.coe EquivLike.toFunLike 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	—	—
semilinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike LinearEquiv.instEquivLike semilinearEquiv	—	—
toAddEquivClass 📖	mathematical	—	AddEquivClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—

(root)

Definitions

Name	Category	Theorems
LinearEquiv 📖	CompData	2063 math math: Pi.comul_eq_adjoint, LinearMap.det_toContinuousLinearMap, DirectSum.IsInternal.ofBijective_coeLinearMap_same, LinearEquiv.multilinearMapCongrLeft_symm_apply, MultilinearMap.domDomCongrLinearEquiv'_symm_apply, continuous_decomposeProdAdjoint, TensorProduct.finsuppRight_apply, LieModule.shiftedGenWeightSpace.shift_apply, DistribMulAction.toModuleAut_apply, LinearMap.lTensor_ker_subtype_tensorKerEquiv_symm, Finsupp.snd_sumFinsuppLEquivProdFinsupp, Rep.resCoindHomEquiv_symm_apply_hom, LinearEquiv.coe_toEquiv, Rep.resCoindHomEquiv_apply_hom, RootPairing.InvariantForm.apply_reflection_reflection, IsLocalizedModule.iso_symm_apply', Polynomial.degreeLT.addLinearEquiv_symm_apply_inr, Finsupp.fst_sumFinsuppLEquivProdFinsupp, LinearMap.restrictScalars_toMatrix, LinearMap.apply_symm_toPerfPair_self, LinearMap.SeparatingRight.toMatrix₂', LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, Submodule.rTensorOne_symm_apply, iSupIndep.linearEquiv_symm_apply, Module.Basis.equivFun_self, TensorProduct.enorm_lid, Module.Basis.coe_map, Submodule.topEquiv_symm_apply_coe, LinearMap.charpoly_def, iSupIndep.dfinsupp_lsum_injective, PiTensorProduct.lift_reindex, DFinsupp.lsum_lsingle, Matrix.toLin_kronecker, QuaternionAlgebra.coe_linearEquivTuple_symm, Matrix.SeparatingLeft.toBilin', LinearMap.detAux_def'', TensorProduct.LieModule.liftLie_apply, LinearEquiv.multilinearMapCongrRight_apply, PiTensorProduct.lift.tprod, IsIsotypic.linearEquiv_fun, Matrix.kroneckerTMulStarAlgEquiv_symm_apply, LinearMap.BilinForm.toMatrix_toBilin, Module.Basis.end_repr_apply, Algebra.Presentation.differentials.comm₁₂_single, Pretrivialization.linearEquivAt_symm_apply, LinearMap.adjoint_adjoint, IsSemisimpleModule.exists_submodule_linearEquiv_quotient, Matrix.SeparatingRight.toLinearMap₂, LinearEquiv.lTensor_pow, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, Rep.MonoidalClosed.linearHomEquiv_symm_hom, MultilinearMap.fromDFinsuppEquiv_apply, LinearEquiv.extendScalarsOfIsLocalizationEquiv_symm_apply, LinearEquiv.ofBijective_symm_apply_apply, LinearEquiv.flip_apply, Complex.linearEquiv_det_conjLIE, LinearEquiv.restrictScalars_apply, TensorProduct.AlgebraTensorModule.rid_symm_apply, PiTensorProduct.liftAlgHom_apply, SimpleGraph.lapMatrix_toLinearMap₂', RootPairing.coroot_eq_polarizationEquiv_apply_root, LinearEquiv.coe_toAddEquiv, MvPolynomial.rTensor_apply_tmul_apply, LinearEquiv.symm_mem_transvections_iff, AlternatingMap.constLinearEquivOfIsEmpty_symm_apply, LinearMap.Nondegenerate.congr, PiTensorProduct.tmulEquiv_symm_apply, dotProductEquiv_symm_apply, LinearEquiv.piCongrRight_apply, addMonoidHomLequivNat_symm_apply, Matrix.separatingRight_toLinearMap₂'_iff, PiTensorProduct.isEmptyEquiv_apply_tprod, QuadraticMap.sum_polar_sub_repr_sq, Module.nonempty_linearEquiv_of_finrank_eq_one, PiTensorProduct.dualDistribEquivOfBasis_symm_apply, MvPolynomial.scalarRTensor_apply_monomial_tmul, Polynomial.toMatrix_sylvesterMap', Module.basisUnique_repr_eq_zero_iff, Matrix.toLinearMapRight'_mul, finsuppTensorFinsupp_apply, TensorPower.cast_cast, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, Module.Basis.equivFun_symm_apply, LinearMap.isPositive_adjoint_comp_self, AddEquiv.toIntLinearEquiv_toAddEquiv, TensorProduct.congr_congr, Matrix.separatingRight_toLinearMap₂_iff, NumberField.Units.fun_eq_repr, Matrix.spectrum_toEuclideanLin, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, LinearMap.rTensor_comm, KaehlerDifferential.polynomialEquiv_symm, TensorProduct.equivFinsuppOfBasisLeft_symm_apply, addMonoidHomLequivInt_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, Module.DualBases.basis_repr_symm_apply, Module.Basis.constr_comp, Module.Basis.constr_symm_apply, LinearMap.BilinForm.toMatrixAux_eq, Orientation.linearEquiv_det_rotation, Algebra.Extension.H1Cotangent.equiv_apply, Finsupp.sumFinsuppLEquivProdFinsupp_apply, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', IsAdjoinRootMonic.coeff_apply, Matrix.toLinearMap₂'_comp, Finsupp.supportedEquivFinsupp_symm_single, PiTensorProduct.lift_reindex_symm, kroneckerTMulAlgEquiv_symm_single_tmul, PiTensorProduct.map_reindex_symm, LinearEquiv.transvection.det_eq_one, WithLp.coe_linearEquiv, Representation.finsupp_apply, LinearMap.toMatrix_apply', LinearMap.toMatrix₂_mul, LinearEquiv.det_trans, ZMod.LFunction_one_sub, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, Module.Basis.dualBasis_coord_toDualEquiv_apply, Matrix.repr_toLin, ZLattice.covolume_eq_det_inv, Submodule.linearEquiv_of_le_sSup, KaehlerDifferential.mvPolynomialBasis_repr_D_X, Submodule.prodEquivOfIsCompl_symm_apply_snd_eq_zero, AlternatingMap.constLinearEquivOfIsEmpty_apply, TensorProduct.sum_tmul_basis_right_injective, Module.Invertible.free_iff_linearEquiv, ZMod.dft_even_iff, PiTensorProduct.reindex_reindex, ZMod.invDFT_apply, LinearEquiv.mapMatrix_apply, PiTensorProduct.subsingletonEquiv_symm_apply, Matrix.liftLinear_single, MulOpposite.coe_opLinearEquiv_symm, LinearEquiv.coe_mk, RootPairing.Equiv.coweightEquiv_symm_coweightMap, TensorProduct.piScalarRight_symm_algebraMap, LinearMap.BilinForm.congr_apply, RootPairing.coreflection_image_eq, LinearMap.BilinForm.toMatrix_compRight, TensorProduct.enorm_comm, CategoryTheory.InducedCategory.homLinearEquiv_apply, SpecialLinearGroup.coe_zpow, LinearEquiv.restrictScalars_symm_apply, LinearMap.adjoint_innerₛₗ_apply, TensorProduct.AlgebraTensorModule.rid_tmul, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, SpecialLinearGroup.toLinearEquiv_symm_to_linearMap, Submodule.dualQuotEquivDualAnnihilator_apply, LinearEquiv.domMulActCongrRight_symm_apply, WittVector.IsocrystalHom.frob_equivariant, LinearEquiv.conj_apply_apply, Algebra.IsPushout.cancelBaseChange_tmul, LinearMap.adjoint_eq_toCLM_adjoint, LinearEquiv.skewSwap_symm_apply, TensorProduct.tensorTensorTensorComm_tmul, exteriorPower.basis_repr_ne, TensorProduct.gradedComm_tmul_one, PolynomialModule.aeval_equivPolynomial, LinearEquiv.coe_withLpCongr, TensorProduct.AlgebraTensorModule.congr_symm_tmul, LinearEquiv.conjAlgEquiv_symm_apply_apply, Matrix.toLinearMap₂_toMatrix₂, LinearMap.toMatrix_one, Module.Basis.mk_repr, starLinearEquiv_symm_apply, LinearMap.isSelfAdjoint_toContinuousLinearMap_iff, SpecialLinearGroup.mem_center_iff_spec, Rep.diagonalHomEquiv_symm_apply, Matrix.separatingRight_toBilin_iff, IsBaseChange.of_fintype_basis_eq, Matrix.spectrum_toLpLin, Finsupp.linearEquivFunOnFinite_symm_coe, Module.Basis.repr_isUnitSMul, LinearEquiv.symm_mem_dilatransvections_iff, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply, ContinuousLinearMap.coprodEquiv_apply, LinearEquiv.map_mem_invtSubmodule_conj_iff, Coalgebra.coassoc_symm_apply, Matrix.toLin_mul_apply, LinearMap.tensorEqLocusEquiv_apply, toMatrix_distrib_mul_action_toLinearMap, ModuleCat.Iso.homCongr_eq_arrowCongr, AlgEquiv.linearEquivConj_mulLeft, LinearMap.BilinForm.toMatrix'_apply, LinearMap.BilinForm.SeparatingRight.toMatrix, LinearMap.nondegenerate_toLinearMap₂'_of_det_ne_zero', MvPolynomial.scalarRTensor_apply_X_tmul_apply, LinearEquiv.congrRight₂_apply, ZMod.dft_mul_const, Shrink.linearEquiv_symm_apply, ULift.moduleEquiv_symm_apply, SpecialLinearGroup.mem_center_iff, Matrix.Nondegenerate.toLinearMap₂, RootPairing.range_weylGroup_coweightHom, Module.Basis.prod_repr_inl, Matrix.kroneckerTMul_assoc', LinearEquiv.cast_symm_apply, ContinuousMultilinearMap.piLinearEquiv_symm_apply, Module.AEval.of_symm_smul, Matrix.intrinsicStar_toLin', Module.Basis.ofZLatticeComap_apply, Submodule.le_linearEquiv_of_sSup_eq_top, LinearMap.coe_toContinuousLinearMap', KaehlerDifferential.polynomialEquiv_D, SemimoduleCat.Iso.homCongr_eq_arrowCongr, linearEquivIsoModuleIso_hom, IsLocalizedModule.iso_symm_apply, continuous_equivFun_basis, TensorProduct.AlgebraTensorModule.rightComm_symm_tmul, Algebra.IsPushout.cancelBaseChange_symm_tmul, Fintype.linearIndependent_iff', isIsotypicOfType_submodule_iff, QuadraticMap.toMatrix'_comp, LinearEquiv.piFinTwo_symm_apply, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, LinearEquiv.conjAlgEquiv_ext_iff', CommRing.Pic.mk_eq_mk_iff, Module.Basis.repr_self_apply, exteriorPower.alternatingMapLinearEquiv_ιMulti, TensorProduct.directSum_lof_tmul_lof, LinearEquiv.coe_inv, IsLocalizedModule.iso_apply_mk, DirectSum.lequivCongrLeft_apply, LinearEquiv.bijective, star_dotProduct_toMatrix₂_mulVec, LocallyConstant.congrRightₗ_symm_apply_apply, IsLocalFrameOn.coeff_apply_of_mem, SpecialLinearGroup.coe_one, MultilinearMap.currySumEquiv_apply, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, LinearMap.sum_repr_mul_repr_mulₛₗ, LinearMap.ringLmapEquivSelf_symm_apply, Module.Basis.equiv_apply, LinearEquiv.dilatransvections_pow_mono, LinearMap.spectrum_toMatrix', Real.smul_map_diagonal_volume_pi, toMatrix_rotation, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, FourierTransform.fourierEquiv_apply, LinearMap.separatingRight_congr_iff, LinearEquiv.rTensor_mul, Derivation.linearEquiv_coe_to_linearMap_comp, 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', Submodule.quotEquivOfEqBot_symm_apply, finsuppTensorFinsupp'_symm_single_eq_tmul_single_one, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, Module.Relations.Solution.IsPresentation.linearEquiv_symm_var, MulOpposite.coe_opLinearEquiv_symm_addEquiv, QuadraticAlgebra.linearEquivTuple_apply, LinearMap.toMatrix_baseChange, RootPairing.toPerfPair_comp_root, TensorProduct.adjoint_map, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, LinearEquiv.conj_comp, LinearIsometryEquiv.lTensor_apply, LinearEquiv.domMulActCongrRight_apply, Rep.coinvariantsTensorFreeLEquiv_symm_apply, LinearEquiv.piCurry_apply, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply, LinearMap.trace_eq_matrix_trace_of_finset, LinearMap.adjoint_toContinuousLinearMap, Finsupp.curryLinearEquiv_symm_apply_apply, Matrix.SeparatingLeft.toLinearMap₂', TensorProduct.dualDistrib_apply_comm, Finsupp.llift_apply, LinearEquiv.coe_symm_toEquiv, LieHom.quotKerEquivRange_toFun, LinearEquiv.conj_refl, Module.reflection_inv, RootPairing.mapsTo_reflection_root, SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, Module.Basis.toDualEquiv_apply, LinearMap.BilinForm.nondegenerate_toMatrix_iff, LinearEquiv.map_zero, Module.equiv_directSum_of_isTorsion, dotProductEquiv_apply_apply, LinearMap.rank_diagonal, TensorProduct.directLimitRight_tmul_of, LinearMap.separatingRight_toMatrix₂'_iff, Matrix.toEuclideanLin_apply, Submodule.biSup_eq_range_dfinsupp_lsum, Algebra.toMatrix_lmul_eq, RootPairing.Equiv.weightHom_toLinearMap, IsIsotypic.submodule_linearEquiv_fun, isAdjointPair_toLinearMap₂, LinearEquiv.congrLeft_symm_apply, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply, TensorProduct.leftComm_tmul, exteriorPower.alternatingMapLinearEquiv_symm_map, LinearEquiv.symm_apply_eq, TensorProduct.comm_comm, Module.Basis.repr_algebraMap, LinearEquiv.one_mem_transvections, Matrix.liftLinear_singleLinearMap, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, Module.AEval'.X_smul_of, Submodule.equivSubtypeMap_symm_apply, Submodule.botEquivPUnit_apply, Matrix.liftLinear_comp_singleLinearMap, Finsupp.basis_repr, Matrix.toBilin_apply, IsLocalRing.basisQuotient_repr, LinearMap.toMatrix₂'_compl₁₂, LinearEquiv.det_baseChange, LinearMap.prodEquiv_apply, Representation.smul_ofModule_asModule, Module.Basis.toLin_toMatrix, WithConv.symm_linearEquiv_apply, Matrix.toLinearEquivRight'OfInv_symm_apply, Pi.counit_eq_adjoint, LinearEquiv.eq_symm_apply, Matrix.toLin'_mul_apply, MultilinearMap.fromDirectSumEquiv_symm_apply, Matrix.toLinearMapₛₗ₂'_single, Matrix.nondegenerate_toBilin'_iff, Representation.coinvariantsFinsuppLEquiv_apply, LinearMap.BilinForm.congr_comp, LinearMap.toMatrixAlgEquiv_apply, GradedTensorProduct.auxEquiv_one, Algebra.TensorProduct.basis_repr_tmul, Basis.linearEquiv_dual_iff_finiteDimensional, RootPairing.reflection_apply_root', LinearMap.toMatrix'_toLin', TensorProduct.toMatrix_assoc, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, Matrix.toLinearMap₂'_apply', Finsupp.LinearEquiv.finsuppUnique_symm_apply, MultilinearMap.domDomCongrLinearEquiv_symm_apply, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, LinearMap.toMatrix_id, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, RootPairing.IsOrthogonal.reflection_apply_left, AddEquiv.toNatLinearEquiv_toAddEquiv, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, LinearEquiv.coe_curry, PositiveLinearMap.preGNS_norm_def, LinearMap.eq_adjoint_iff_basis_left, PositiveLinearMap.leftMulMapPreGNS_apply, Matrix.mul_reindexLinearEquiv_one, LinearEquiv.image_symm_eq_preimage, Module.Invertible.exists_linearEquiv_ideal, TensorPower.algebraMap₀_mul, LinearEquiv.coe_toLinearMap_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, PiTensorProduct.reindex_comp_tprod, LinearIsometryEquiv.coe_toLinearEquiv, TensorProduct.equivFinsuppOfBasisRight_apply_tmul, Submodule.coe_prodEquivOfIsCompl', Module.Basis.ofEquivFun_repr_apply, TensorProduct.congr_zpow, Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap, Module.Basis.sumQuot_repr_left, LinearEquiv.ofSubmodules_apply, Submodule.topEquiv_apply, Coalgebra.comm_comul, Module.Relations.Solution.IsPresentation.linearEquiv_apply, Module.Basis.reindexRange_repr', Module.reflection_apply_self, Polynomial.degreeLT.addLinearEquiv_castAdd, KaehlerDifferential.polynomialEquiv_comp_D, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LinearEquiv.toSpanNonzeroSingleton_homothety, Module.Basis.reindexRange_repr, IsBaseChange.endHom_toMatrix, DistribMulAction.toLinearEquiv_symm_apply, LocalizedModule.equivTensorProduct_apply_mk, ModuleCat.homLinearEquiv_symm_apply, Real.map_matrix_volume_pi_eq_smul_volume_pi, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul, Module.Basis.toMatrix_map, PiTensorProduct.ofFinsuppEquiv'_tprod_single, TensorProduct.lidIsometry_apply, LinearEquiv.mul_eq_trans, MultilinearMap.curryFinFinset_apply, LinearEquiv.refl_mem_transvections, LinearEquiv.lTensor_zpow, IsNoetherian.equivPUnitOfProdInjective_apply, StrongDual.toWeakDual_inj, LinearMap.BilinForm.Nondegenerate.congr, Rep.MonoidalClosed.linearHomEquivComm_hom, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, LinearMap.tensorKerEquivOfSurjective_symm_tmul, SemimoduleCat.homLinearEquiv_apply, TensorProduct.equivFinsuppOfBasisLeft_symm, LinearMap.IsProj.eq_conj_prodMap, Module.Basis.coe_toOrthonormalBasis_repr, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, 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, ModularGroup.lcRow0Extend_symm_apply, RootPairing.reflection_same, LinearMap.extendScalarsOfIsLocalizationEquiv_apply, LinearEquiv.skewSwap_apply, LocalizedModule.equivTensorProduct_symm_apply_tmul, LinearEquiv.arrowCongr_symm_apply, TensorProduct.finsuppScalarRight_apply_tmul, Representation.single_smul, ContinuousLinearMap.toUniformConvergenceCLM_apply, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, Module.FinitePresentation.linearEquivMap_symm_apply, MulOpposite.coe_opLinearEquiv_addEquiv, Matrix.conjTransposeLinearEquiv_apply, Matrix.isNilpotent_toLin'_iff, Orientation.volumeForm_zero_pos, Module.Basis.constrL_apply, Module.AEval'.of_symm_X_smul, homTensorHomEquiv_apply, LinearEquiv.zero_symm, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, Matrix.toLinearEquiv'_symm_apply, PiTensorProduct.subsingletonEquiv_apply_tprod, LinearEquiv.uniqueProd_apply, DFinsupp.sigmaCurryLEquiv_apply, LinearMap.BilinForm.mul_toMatrix'_mul, Trivialization.linearEquivAt_apply, finsuppTensorFinsupp'_single_tmul_single, Finsupp.mapDomain.coe_linearEquiv, LocallyConstant.congrRightₗ_apply_apply, NumberField.canonicalEmbedding.integralBasis_repr_apply, BilinForm.mul_toMatrix_mul, QuadraticForm.tensorRId_symm_apply, Module.Invertible.rTensorEquiv_apply_apply, Rep.coindVEquiv_symm_apply_coe, LinearEquiv.lTensor_tmul, RootPairing.coreflection_inv, Module.Basis.linearMap_apply, CoalgEquiv.coe_toLinearEquiv, Matrix.toLinearMap₂_compl₁₂, LinearEquiv.coe_neg, TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul, LinearEquiv.mem_dilatransvections_iff_rank, PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod, basisOfLinearIndependentOfCardEqFinrank_repr_apply, Module.Invertible.linearEquivOfRightInverse_symm_apply, PiTensorProduct.ofFinsuppEquiv_tprod_single, LinearEquiv.rTensor_zpow, LinearMap.lsum_apply, LinearEquiv.funUnique_symm_apply, Module.Ray.linearEquiv_smul_eq_map, LinearEquiv.coe_ofInjectiveEndo, LinearMap.toLinearMap_toContPerfPair, continuous_decomposeProdAdjoint_symm, 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, Matrix.piLinearEquiv_apply, ZMod.dft_comp_unitMul, LinearMap.toMatrix₂_compl₂, finsuppTensorFinsuppLid_symm_single_smul, Module.reflection_mul_reflection_pow_apply, DFinsupp.sum_mapRange_index.linearMap, PiTensorProduct.congr_symm_tprod, rTensorHomEquivHomRTensor_apply, TensorPower.algebraMap₀_one, ExteriorAlgebra.liftAlternatingEquiv_apply, RootPairing.Equiv.coweightHom_injective, dualTensorHomEquivOfBasis_symm_cancel_right, LinearMap.GeneralLinearGroup.ofLinearEquiv_inv, LinearEquiv.coe_pow, Matrix.toLpLin_symm_pow, MvPolynomial.scalarRTensor_apply_tmul, TensorProduct.prodLeft_tmul, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', finsuppTensorFinsupp'_symm_single_mul, LinearEquiv.ofLeftInverse_symm_apply, isOpenMap_toWeakSpace_symm, LinearMap.polyCharpolyAux_map_eval, SpecialLinearGroup.coe_inv, Matrix.toLinearMapₛₗ₂'_aux_eq, ZSpan.repr_ceil_apply, KaehlerDifferential.linearMapEquivDerivation_apply_apply, ZLattice.comap_equiv_apply, Matrix.linfty_opNNNorm_toMatrix, KaehlerDifferential.tensorKaehlerEquivBase_tmul, Module.Basis.coe_constrL, MulOpposite.isometry_opLinearEquiv, LinearEquiv.comp_symm_eq, Submodule.botEquivPUnit_symm_apply, TensorProduct.map_map_assoc_symm, Module.Basis.addSubgroupOfClosure_repr_apply, Algebra.traceForm_toMatrix, KaehlerDifferential.tensorKaehlerEquivBase_symm_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply, basis_toMatrix_basisFun_mul, Matrix.toLin_scalar, GradedTensorProduct.auxEquiv_symm_one, LinearMap.adjoint_rTensor, GradedTensorProduct.auxEquiv_comm, TensorProduct.finsuppLeft_symm_apply_single, Finsupp.linearEquivFunOnFinite_symm_apply, LinearEquiv.mul_apply, LinearMap.adjoint_inner_right, RootPairing.reflection_sq, BilinForm.dotProduct_toMatrix_mulVec, LinearEquiv.multilinearMapCongrRight_symm_apply, Module.invOn_reflection_of_mapsTo, LinearEquiv.piUnique_symm_apply, MultilinearMap.coe_currySumEquiv_symm, LinearEquiv.eq_symm_comp, CommRing.Pic.mk_eq_iff, IsTensorProduct.equiv_symm_apply, Matrix.toLpLin_one, Convex.toWeakSpace_closure, finsuppTensorFinsupp'_apply_apply, MultilinearMap.curryFinFinset_symm_apply_piecewise_const, PiTensorProduct.ofFinsuppEquiv_symm_single_tprod, Module.Basis.reindexRange_repr_self, LinearMap.isPosSemidef_iff_posSemidef_toMatrix, LinearEquiv.ofSubmodule'_symm_apply, PositiveLinearMap.preGNS_inner_def, LinearEquiv.surjective, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, TensorProduct.prodLeft_symm_tmul, RootPairing.Equiv.weightEquiv_apply, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply, LinearEquiv.rTensor_refl_apply, Polynomial.degreeLT.addLinearEquiv_apply_snd, KaehlerDifferential.linearMapEquivDerivation_symm_apply, TensorProduct.inner_lid_lid, LinearMap.BilinForm.tensorDistribEquiv_apply, LinearEquiv.mem_transvections_iff, Matrix.piLp_ofLp_toEuclideanLin, LinearMap.BilinForm.toMatrix_apply, Module.Basis.sumQuot_repr_inl, LinearEquiv.piUnique_apply, LinearEquiv.sumPiEquivProdPi_apply, TensorProduct.norm_comm, LinearEquiv.invFun_eq_symm, CliffordAlgebra.changeFormEquiv_apply, PowerBasis.constr_pow_algebraMap, lieEquivMatrix'_apply, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, TensorProduct.dualDistribEquivOfBasis_symm_apply, BilinForm.toMatrix_toBilin, WeakDual.isCompact_closedBall, IsLocalizedModule.linearEquiv_apply, Matrix.toPerfectPairing_apply_apply, LinearMap.quotientInfEquivSupQuotient_apply_mk, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, SpecialLinearGroup.congr_linearEquiv_coe_apply, Module.DirectLimit.congr_symm_apply_of, LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr, Algebra.Generators.cotangentSpaceBasis_repr_tmul, LinearEquiv.funCongrLeft_apply, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, LinearMap.minpoly_toMatrix', LinearMap.liftBaseChangeEquiv_symm_apply, RootPairing.RootPositiveForm.isOrthogonal_reflection, Algebra.TensorProduct.equivFinsuppOfBasis_apply, LinearMap.toMatrix₂_comp, Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl, TensorProduct.gradedComm_algebraMap, AffineEquiv.map_vadd, Matrix.SeparatingRight.toLinearMap₂', Representation.asModuleEquiv_symm_map_smul, TensorProduct.norm_assoc, LinearEquiv.transvection.apply, Module.Basis.repr_linearCombination, SpecialLinearGroup.det_eq_one, TensorProduct.assoc_tmul, WittVector.IsocrystalEquiv.frob_equivariant, PiTensorProduct.reindex_tprod, Submodule.mem_iSup_iff_exists_dfinsupp, Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply, QuadraticForm.tensorRId_apply, MvPolynomial.rTensor_apply_X_tmul, LinearMap.prodEquiv_symm_apply, 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, LinearEquiv.extendScalarsOfSurjective_apply, InnerProductSpace.AlgebraOfCoalgebra.mul_def, LinearMap.BilinForm.separatingRight_toMatrix'_iff, Matrix.isUnit_toLin'_iff, Module.piEquiv_apply_apply, LinearIndependent.linearCombinationEquiv_apply_coe, TensorProduct.AlgebraTensorModule.leftComm_tmul, IsIsotypicOfType.linearEquiv_fun, Matrix.toLin'_mul, Submodule.iSup_eq_range_dfinsupp_lsum, ModularGroup.lcRow0Extend_apply, 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, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, LinearMap.IsReflective.reflective_reflection, Matrix.ofLp_toLpLin, TensorPower.galgebra_toFun_def, Module.range_piEquiv, LinearEquiv.cast_apply, CommRing.Pic.ext_iff, StarModule.decomposeProdAdjoint_symm_apply, Module.Basis.dualBasis_equivFun, LinearEquiv.coe_toAddEquiv_symm, LinearMap.toMatrix_smulBasis_left, Module.Basis.coe_toOrthonormalBasis_repr_symm, TensorProduct.congr_tmul, LinearMap.GeneralLinearGroup.toLinearEquiv_inv, LinearMap.BilinForm.isSymm_iff_flip, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, MultilinearMap.fromDFinsuppEquiv_single, LinearMap.det_toLin', Submodule.linearEquiv_det_reflection, DirectSum.coe_congr_linearEquiv, coe_toLexLinearEquiv, LinearEquiv.rTensor_pow, LinearMap.SeparatingRight.congr, LinearEquiv.symm_apply_apply, Matrix.rank_eq_finrank_range_toLin, MvPolynomial.rTensor_apply_tmul, TensorProduct.AlgebraTensorModule.congr_mul, Matrix.toLinearMapRight'_mul_apply, CommRing.Pic.mk_eq_one_iff, BilinForm.toMatrix_comp, CharacterModule.intSpanEquivQuotAddOrderOf_apply, Matrix.reindexLinearEquiv_one, PiTensorProduct.norm_eval_le_injectiveSeminorm, FiniteDimensional.basisSingleton_repr_apply, Subalgebra.linearEquivOp_apply_coe, Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero, Matrix.toLin_mul, TensorProduct.AlgebraTensorModule.assoc_tmul, LinearEquiv.coe_prodUnique, Matrix.toLin_pow, Submodule.coe_tensorSpanEquivSpan_apply_tmul, Module.Basis.equivFunL_symm_apply_repr, LinearEquiv.baseChange_mul, Submodule.FG.lTensor.directLimit_apply', TensorProduct.directSumLeft_tmul_lof, PowerBasis.repr_gen_pow_isIntegral, LinearEquiv.trans_apply, Matrix.toLin_self, kroneckerTMulLinearEquiv_one, TensorProduct.AlgebraTensorModule.leftComm_symm_tmul, Module.DirectLimit.linearEquiv_of, Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, Finsupp.lsum_single, PositiveLinearMap.toPreGNS_ofPreGNS, LinearMap.BilinForm.sum_repr_mul_repr_mul, Finsupp.linearEquivFunOnFinite_single, Module.Basis.mulOpposite_repr_op, TensorProduct.AlgebraTensorModule.rightComm_tmul, LinearMap.separatingLeft_toMatrix₂'_iff, LinearEquiv.transvections_subset_dilatransvections, Module.Basis.smulTower'_repr_mk, Function.Exact.split_tfae, LinearEquiv.map_smulₛₗ, TensorProduct.AlgebraTensorModule.assoc_symm_tmul, 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, Orientation.map_eq_det_inv_smul, TensorProduct.lid_symm_apply, IsTensorProduct.equiv_apply, Matrix.toLinearMapₛₗ₂'_toMatrix', LinearMap.toMatrix'_algebraMap, TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, Rep.resIndAdjunction_homEquiv_symm_apply, finsuppTensorFinsupp_single, PiTensorProduct.liftEquiv_symm_apply, LocalizedModule.coe_map_eq, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, RootPairing.bijOn_reflection_root, Module.Basis.equiv'_symm_apply, LinearMap.IsReflective.isOrthogonal_reflection, Module.reflection_mul_reflection_pow, Module.Basis.repr_reindex, BilinearForm.toMatrixAux_eq, TensorProduct.lid_tmul, RootPairing.rootForm_reflection_reflection_apply, Matrix.SeparatingLeft.toBilin, Matrix.charpoly_toLin, Module.subsingletonEquiv_symm_apply, LinearEquiv.toLinearMap_injective, LinearEquiv.extendScalarsOfIsLocalization_symm_apply, LinearEquiv.congrLeft_apply, Module.Basis.algebraMapCoeffs_repr_apply_toFun, QuadraticForm.tmul_tensorAssoc_apply, LinearEquiv.piRing_symm_apply, Module.DirectLimit.congr_apply_of, LinearMap.toMatrix_mulVec_repr, LinearMap.toMatrix_innerₛₗ_apply, TensorProduct.piRight_symm_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, RootPairing.Equiv.weightEquiv_mul, IsLocalizedModule.mapEquiv_apply, Submodule.span_image_linearEquiv, Matrix.nondegenerate_toBilin_iff, LinearEquiv.det_symm, LinearIsometryEquiv.toLinearEquiv_injective, LinearMap.range_toContinuousLinearMap, WithCStarModule.linearEquiv_apply, Polynomial.mkDerivationEquiv_symm_apply, TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul, Matrix.toLin'_reindex, LinearMap.BilinForm.toDual_def, Module.Relations.Solution.IsPresentation.uniq_var, Module.Basis.algebraMapCoeffs_repr_apply_apply, LinearEquiv.ofInjective_apply, Matrix.PosSemidef.toLinearMap₂'_zero_iff, MultilinearMap.domDomCongrLinearEquiv_apply, LinearMap.BilinForm.toMatrix'_compLeft, Matrix.toLinearMapₛₗ₂_apply, MultilinearMap.freeDFinsuppEquiv_single, WeakDual.isSeqCompact_closedBall, LinearMap.BilinForm.dualBasis_repr_apply, PiTensorProduct.liftEquiv_apply, IsIsotypicOfType.linearEquiv_finsupp, LinearEquiv.ofBijective_apply, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, ContinuousMultilinearMap.piLinearEquiv_apply, Complex.selfAdjointEquiv_apply, LinearMap.isSelfAdjoint_iff', Orientation.areaForm'_apply, Submodule.comap_equiv_self_of_inj_of_le_apply, DirectSum.linearEquivFunOnFintype_lof, Module.Basis.sumQuot_repr_inl_of_mem, Module.Basis.end_apply, Rep.freeLiftLEquiv_apply, TensorPower.algebraMap₀_eq_smul_one, Submodule.set_smul_eq_map, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, Matrix.Nondegenerate.toBilin, TensorProduct.finsuppScalarRight_apply_tmul_apply, LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero, AlgEquiv.coe_symm_toLinearEquiv, LinearMap.toMatrix'_apply, LinearEquiv.baseChange_tmul, PiTensorProduct.ofDFinsuppEquiv_tprod_apply, QuadraticForm.tmul_tensorComm_apply, Module.Basis.repr_symm_single, Matrix.toLpLin_toLp, apply_eq_dotProduct_toMatrix₂_mulVec, Polynomial.degreeLT.addLinearEquiv_apply, Module.reflection_reflection_iterate, LinearEquiv.mem_dilatransvections_iff_finrank, kroneckerLinearEquiv_symm_kronecker, Submodule.quotEquivOfEqBot_apply_mk, LinearMap.coe_toContinuousLinearMap, LinearEquiv.coe_toContinuousLinearEquiv', LinearMap.BilinForm.separatingRight_toMatrix_iff, MultilinearMap.freeDFinsuppEquiv_def, TensorProduct.finsuppLeft_apply, ContinuousLinearMap.toSpanSingletonLE_apply, LinearMap.BilinForm.SeparatingLeft.toMatrix', finsuppTensorFinsuppRid_symm_single_smul, LinearEquiv.prodComm_apply, TensorProduct.prodRight_symm_tmul, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearEquiv.conj_apply, DFinsupp.mapRange.linearEquiv_apply, LinearEquiv.ofSubmodules_symm_apply, IsSemisimpleModule.exists_quotient_linearEquiv_submodule, Complex.equivRealProdLm_apply, LinearMap.kerComplementEquivRange_apply_coe, Submodule.restrictScalarsEquiv_symm_apply, ZMod.invDFT_def', Module.Basis.restrictScalars_repr_apply, Matrix.ker_toLin_eq_bot, SpecialLinearGroup.det_coe, RootPairing.Equiv.weightEquiv_inv, Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp, Module.Basis.equivFunL_apply, Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff, GradedTensorProduct.auxEquiv_mul, Fintype.linearIndependent_iff'ₛ, QuadraticForm.tmul_tensorRId_apply, LinearMap.IsSymmetric.adjoint_eq, TensorProduct.piRight_symm_single, Module.FinitePresentation.linearEquivMap_apply, FourierTransform.fourierEquiv_symm_apply, LinearIsometryEquiv.coe_symm_toLinearEquiv, LinearEquiv.coe_toAffineEquiv, IsLocalizedModule.mapEquiv_symm_apply, Module.Invertible.linearEquivOfLeftInverse_symm_apply, ProperCone.dual_singleton, Module.involutive_reflection, Algebra.TensorProduct.basisAux_tmul, Module.Basis.singleton_repr, TensorProduct.map_comm, LinearEquiv.coe_toContinuousLinearEquiv_symm', Submodule.le_linearEquiv_of_le_sSup, Module.AEval.X_pow_smul_of, linearEquivIsoModuleIsoₛ_hom, 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, LinearEquiv.toSpanNonzeroSingleton_apply, Matrix.kroneckerTMulAlgEquiv_symm_apply, ContinuousLinearEquiv.coe_toLinearEquiv, Polynomial.mkDerivationEquiv_apply, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, Rep.resIndAdjunction_homEquiv_apply, RootPairing.Equiv.coweightEquiv_mul, RootPairing.toPerfPair_flip_comp_coroot, DFinsupp.linearEquivFunOnFintype_symm_apply, LinearMap.toMatrix_transpose_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, Pi.basis_repr, Matrix.kroneckerTMulStarAlgEquiv_apply, toMatrix_dualTensorHom, LinearEquiv.arrowCongr_apply, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, Algebra.Generators.H1Cotangent.δAux_ofComp, LinearMap.isPositive_toContinuousLinearMap_iff, Matrix.range_toLin', LinearEquiv.apply_smulCommClass, LinearEquiv.finTwoArrow_apply, Submodule.prodEquivOfIsCompl_symm_apply, ZMod.dft_apply, LinearEquiv.skewProd_symm_apply, Submodule.Quotient.restrictScalarsEquiv_symm_mk, LinearMap.mul_toMatrix', Matrix.liftLinear_apply, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, InnerProductSpace.gramSchmidt_triangular, PiTensorProduct.lift_comp_reindex, QuadraticAlgebra.basis_repr_apply, PiTensorProduct.dualDistribEquivOfBasis_apply_apply, LinearMap.star_eq_adjoint, LinearEquiv.conjRingEquiv_apply_apply, LinearMap.toMatrix_smulBasis_right, Matrix.toLpLin_symm_id, Module.Basis.toDual_eq_repr, Matrix.range_toLin_eq_top, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, TensorProduct.lid'_apply_tmul, Matrix.toLin_finTwoProd_apply, Rep.leftRegularHomEquiv_symm_apply, Module.Basis.sum_repr_mul_repr, Matrix.isPositive_toEuclideanLin_iff, RootPairing.coreflection_apply_self, LinearEquiv.symm_trans_apply, ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap, RootPairing.polarizationEquiv_apply, FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq, NumberField.integralBasis_repr_apply, LinearMap.mul_toMatrix₂, RootPairing.Equiv.coweightEquiv_inv, TensorProduct.inner_assoc_assoc, kroneckerTMulLinearEquiv_mul, QuadraticMap.discr_comp, Module.Basis.linearMap_repr_apply, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, LinearEquiv.baseChange_zpow, kroneckerTMulLinearEquiv_symm_kroneckerTMul, LinearEquiv.zero_apply, MultilinearMap.curryFinFinset_apply_const, RootPairing.bijOn_coreflection_coroot, MultilinearMap.freeFinsuppEquiv_def, LinearMap.lsum_single, LinearMap.nondegenerate_congr_iff, Rep.coindResAdjunction_homEquiv_apply, ZMod.invDFT_apply', SpecialLinearGroup.coe_mul, LinearMap.toMatrix'_mul, LinearMap.adjoint_toSpanSingleton, mul_basis_toMatrix, LinearEquiv.image_eq_preimage_symm, Module.dualProdDualEquivDual_apply_apply, Submodule.quotientPi_apply, Submodule.rTensorOne_tmul, FiniteDimensional.nonempty_linearEquiv_of_finrank_eq, ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply, LinearIsometryEquiv.withLpProdCongr_symm_apply, LinearEquiv.conj_symm_conj, LinearMap.toMatrix_algebraMap, LinearEquiv.coe_curry_symm, LinearMap.spectrum_toMatrix, PowerBasis.constr_pow_gen, LinearEquiv.refl_mem_dilatransvections, IsBaseChange.equiv_symm_apply, TensorProduct.congr_symm_tmul, LinearMap.SeparatingRight.toMatrix₂, Matrix.isUnit_toLin_iff, Polynomial.degreeLT.addLinearEquiv_apply', Matrix.uniqueLinearEquiv_apply, Representation.ofMulActionSelfAsModuleEquiv_apply, Subspace.quotAnnihilatorEquiv_apply, Matrix.diagonal_toLin', LinearMap.re_inner_adjoint_mul_self_nonneg, TensorPower.mul_one, exteriorPower.oneEquiv_symm_apply, LinearMap.isPositive_self_comp_adjoint, QuadraticForm.tensorLId_symm_apply, Matrix.charpoly_toLin', Matrix.toLinearMap₂'_toMatrix', PiTensorProduct.ofFinsuppEquiv_apply, LinearEquiv.piCongrLeft'_symm_apply, Matrix.toLinearMapₛₗ₂'_apply, TensorProduct.finsuppScalarRight_symm_apply_single, Algebra.Extension.H1Cotangent.equivOfFormallySmooth_apply, LinearEquiv.submoduleMap_apply, Matrix.toLin'_pow, RootPairing.IsOrthogonal.reflection_apply_right, Module.Basis.mem_span_image, LinearIsometryEquiv.toLinearEquiv_smul, LinearEquiv.symm_smul, LinearMap.BilinForm.SeparatingLeft.toMatrix, LinearEquiv.rTensor_symm_tmul, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, LinearEquiv.transvections_pow_mono, Module.Basis.localizationLocalization_repr_algebraMap, Complex.equivRealProdLm_symm_apply, Matrix.l2_opNNNorm_def, LinearMap.lTensor_comm, LinearEquiv.det_conj, Module.Basis.dualBasis_apply, LinearMap.apply_toPerfPair_flip, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, RootPairing.Equiv.weightHom_apply, WithCStarModule.linearEquiv_symm_apply, Complex.equivRealProdLm_symm_apply_im, apply_eq_star_dotProduct_toMatrix₂_mulVec, tensorKaehlerQuotKerSqEquiv_tmul_D, LinearMap.toMatrix_mul, Complex.coe_basisOneI_repr, LinearMap.toMatrix₂_compl₁₂, TensorProduct.tensorQuotientEquiv_apply_mk_tmul, Matrix.minpoly_toLin', Module.Basis.reindexFinsetRange_repr_self, LinearEquiv.symm_comp_eq, IsLocalizedModule.linearEquiv_symm_apply, LinearMap.equivProdOfSurjectiveOfIsCompl_apply, 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', SpecialLinearGroup.coe_pow, Module.Basis.repr_symm_single_one, Submodule.linearEquiv_of_sSup_eq_top, LinearMap.toMatrix'_intrinsicStar, LinearMap.BilinForm.congr_congr, Matrix.compLinearEquiv_symm_apply, QuadraticForm.tensorComm_apply, Submodule.prodEquivOfIsCompl_symm_apply_left, LinearEquiv.lieConj_apply, IsBaseChange.linearMapLeftRightHom_toMatrix, Submodule.quotientEquivOfIsCompl_apply_mk_coe, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, DFinsupp.lsum_single, LinearEquiv.uniqueProd_symm_apply, Matrix.toLinOfInv_symm_apply, LinearMap.toMatrix_smulRight, kroneckerTMulLinearEquiv_tmul, LinearEquiv.alternatingMapCongrRight_apply_apply, LinearMap.toMatrix₂Aux_eq, LinearEquiv.extendScalarsOfIsLocalizationEquiv_apply, 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', Algebra.IsPushout.cancelBaseChangeAux_symm_tmul, Representation.asModuleEquiv_symm_map_rho, RootPairing.Base.toCoweightBasis_repr_coroot, LinearMap.isPairSelfAdjoint_equiv, 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, LinearMap.quotKerEquivRange_symm_apply_image, Finsupp.lsum_apply, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LinearMap.SeparatingLeft.toMatrix₂, LinearMap.toMatrix'_toLinearMap₂', Basis.multilinearMap_apply_apply, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, PolynomialModule.equivPolynomial_single, BilinForm.toMatrix_mul_basis_toMatrix, WeakDual.isClosed_closedBall, Submodule.Quotient.equiv_symm_apply, iSupIndep.linearEquiv_apply, Module.Basis.coe_finTwoProd_repr, LinearMap.BilinForm.mul_toMatrix', QuadraticForm.tensorAssoc_symm_apply, ContinuousLinearEquiv.toLinearEquiv_smul, PiTensorProduct.isEmptyEquiv_symm_apply, DistribMulAction.toLinearEquiv_apply, LinearEquiv.map_add, PiTensorProduct.subsingletonEquiv_symm_apply', Finsupp.coe_lsum, ContinuousLinearEquiv.coe_mk, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, LinearMap.toMatrixRight'_id, TensorProduct.rid_tmul, CategoryTheory.Linear.homCongr_apply, LinearEquiv.symm_bijective, LinearMap.minpoly_toMatrix, CharacterModule.homEquiv_symm_apply_apply_apply, AffineEquiv.linearHom_apply, LinearMap.adjoint_lTensor, Matrix.nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, LinearEquiv.smulOfNeZero_apply, multilinearCurryLeftEquiv_apply, starL'_symm_apply, Module.reflection_mul_reflection_pow_apply_self, PiTensorProduct.tmulEquivDep_symm_apply, Submodule.rTensorOne_tmul_one, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, IsAdjoinRootMonic.coeff_apply_lt, MultilinearMap.constLinearEquivOfIsEmpty_apply, LinearEquiv.finTwoArrow_symm_apply, LinearEquiv.map_dfinsuppSumAddHom, DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, Module.dualProdDualEquivDual_apply, Module.Basis.toMatrix_apply, RootPairing.Hom.weight_coweight_transpose_apply, MultilinearMap.curryFinFinset_symm_apply_const, KaehlerDifferential.mvPolynomialBasis_repr_apply, LinearEquiv.coe_symm_mk, Finsupp.sigmaFinsuppLEquivPiFinsupp_apply, CategoryTheory.Iso.toLinearEquiv_apply, finsuppTensorFinsuppRid_single_tmul_single, LinearIndependent.linearCombinationEquiv_symm_apply, Submodule.equivSubtypeMap_apply, Module.DualBases.basis_repr_apply, LinearEquiv.toLinearMap_eq_coe, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, SpecialLinearGroup.congr_linearEquiv_apply_apply, Algebra.toMatrix_lmul', DFinsupp.sigmaCurryLEquiv_symm_apply, toWeakSpace_closedConvexHull_eq, Algebra.Extension.contangentEquiv_tmul, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, LieModuleEquiv.coe_toLinearEquiv, Finsupp.llift_symm_apply, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, AffineMap.toConstProdLinearMap_apply, LinearMap.quotKerEquivRange_apply_mk, TensorProduct.finsuppScalarLeft_apply_tmul_apply, Matrix.ker_diagonal_toLin', TensorProduct.inner_comm_comm, AddEquiv.coe_toLinearEquiv_symm, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply, Module.Basis.map_apply, Module.Basis.symmetricAlgebra_repr_apply, LinearEquiv.prodProdProdComm_apply, LinearEquiv.toEquiv_injective, Module.AEval.of_symm_X_smul, LinearEquiv.sumPiEquivProdPi_symm_apply, FGModuleCat.Iso.conj_eq_conj, Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val, Complex.linearEquiv_det_conjAe, ZLattice.exists_forall_abs_repr_le_norm, LinearEquiv.symmEquiv_apply_apply, Matrix.toBilin'_apply, Function.Exact.split_tfae', MultilinearMap.domDomCongrLinearEquiv'_apply, LieAlgebra.conj_ad_apply, isSimpleModule_iff_quot_maximal, LinearMap.toMatrix_prodMap, Matrix.toLin_apply, Matrix.toLin'_one, PiTensorProduct.tmulEquivDep_apply, Polynomial.toFinsuppIsoLinear_apply, Algebra.TensorProduct.linearEquivIncludeRange_symm_tmul, MultilinearMap.freeFinsuppEquiv_apply, AlgEquiv.linearEquivConj_mulLeftRight, Module.Basis.constr_apply_fintype, LinearEquiv.symm_conj_apply, MultilinearMap.ofSubsingletonₗ_apply, DFinsupp.lsum_symm_apply, LinearEquiv.restrictScalars_injective, ZMod.dft_dft, WithConv.linearEquiv_apply, AlgEquiv.coe_toLinearEquiv, LinearEquiv.conjAlgEquiv_apply_apply, MultilinearMap.fromDirectSumEquiv_apply, LinearEquiv.algEquivOfRing_symm_apply, Matrix.reindexLinearEquiv_mul, Module.Basis.smul_eq_map, finsuppLEquivDirectSum_single, TensorProduct.assocIsometry_apply, Matrix.toLin_conjTranspose, Submodule.quotientEquivOfIsCompl_symm_apply, Module.Relations.Solution.IsPresentation.uniq_symm_var, LinearEquiv.conj_conj_symm, GradedTensorProduct.auxEquiv_tmul, Ideal.cotangentEquivIdeal_apply, AdicCompletion.congr_symm_apply, LinearEquiv.ofSubsingleton_apply, LinearIsometryEquiv.rTensor_apply, PolynomialModule.equivPolynomialSelf_apply_eq, LinearEquiv.coe_ofEq_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply, LinearEquiv.eq_comp_symm, SpecialLinearGroup.centerEquivRootsOfUnity_apply, AffineMap.toConstProdLinearMap_symm_apply, PiTensorProduct.ofDFinsuppEquiv_tprod_single, LinearEquiv.smul_apply, DirectSum.decomposeLinearEquiv_apply, LinearMap.BilinForm.nondegenerate_congr_iff, exteriorPower.alternatingMapLinearEquiv_comp, Matrix.trace_toLin'_eq, TensorProduct.gradedComm_of_zero_tmul, LocallyConstant.congrLeftₗ_symm_apply_apply, Matrix.toLin'OfInv_symm_apply, Orientation.rotation_eq_matrix_toLin, LinearMap.BilinForm.flip_apply, Module.Basis.sumQuot_repr_inr_of_mem, AlternatingMap.domDomCongrₗ_toAddEquiv, AffineEquiv.ofLinearEquiv_apply, QuadraticAlgebra.linearEquivTuple_symm_apply, Module.Basis.repr_injective, Module.FinitePresentation.linearEquivMapExtendScalars_apply, IsLocalizedModule.iso_symm_apply_aux, IsBaseChange.endHom_apply, Module.Basis.parallelepiped_eq_map, LinearEquiv.one_mem_dilatransvections, TensorProduct.piScalarRight_symm_single, LinearEquiv.toLinearMap_smul, LinearEquiv.map_eq_zero_iff, Module.Basis.repr_apply_eq, ContinuousAlternatingMap.piLinearEquiv_symm_apply, TensorPower.algebraMap₀_mul_algebraMap₀, TensorPower.gMul_def, LinearEquiv.isUnit_det, LinearMap.polyCharpolyAux_map_aeval, TensorProduct.directSumLeft_tmul, Algebra.traceMatrix_of_basis, LinearEquiv.prodUnique_symm_apply, TensorProduct.quotTensorEquivQuotSMul_symm_mk, AdicCompletion.of_ofLinearEquiv_symm, Trivialization.coordChangeL_symm_apply, SpecialLinearGroup.toLinearEquiv_symm_apply, NumberField.inverse_basisMatrix_mulVec_eq_repr, Matrix.spectrum_toLin, LinearEquiv.apply_smulCommClass', LinearMap.toMatrix'_comp, Matrix.toLinearEquiv'_apply, LinearMap.isUnit_toMatrix'_iff, Submodule.quotientPi_symm_apply, 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, LinearMap.BilinForm.comp_congr, Matrix.toBilin'_comp, Matrix.isHermitian_iff_isSymmetric, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', MultilinearMap.freeFinsuppEquiv_single, LinearMap.kerComplementEquivRange_symm_apply, Module.AEval.X_smul_of, LinearMap.separatingLeft_congr_iff, Module.Basis.end_repr_symm_apply, LinearMap.GeneralLinearGroup.coe_ofLinearEquiv, Module.evalEquiv_apply, InnerProductSpace.toMatrix_rankOne, QuadraticForm.tmul_tensorLId_apply, PeriodPair.latticeEquiv_symm_apply, MvPolynomial.rTensor_symm_apply_single, Complex.equivRealProdLm_symm_apply_re, Module.Basis.equiv'_apply, CStarMatrix.reindexₗ_apply, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, QuadraticForm.tensorLId_apply, LinearMap.mul_toMatrix₂_mul, LinearEquiv.coord_self, Finsupp.lcongr_symm_single, Module.Basis.apply_eq_iff, sigmaFinsuppLequivDFinsupp_symm_apply, LinearMap.BilinForm.tensorDistribEquiv_tmul, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, LinearMap.eq_adjoint_iff_basis, TensorProduct.leftComm_symm_tmul, RootPairing.coreflection_sq, QuotSMulTop.equivQuotTensor_naturality_mk, DirectSum.decomposeLinearEquiv_symm_apply, LinearEquiv.ofLeftInverse_apply, LinearMap.toMatrix'_id, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearMap.polyCharpolyAux_coeff_eval, RingEquiv.toSemilinearEquiv_symm_apply, LinearEquiv.baseChange_inv, RootPairing.Equiv.coweightHom_op, LinearEquiv.coe_ofInvolutive, LinearEquiv.symmEquiv_symm_apply_apply, SemimoduleCat.Iso.conj_eq_conj, LinearMap.BilinForm.mul_toMatrix_mul, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, Matrix.toLinAlgEquiv_apply, Module.Basis.coe_ofRepr, LinearMap.nondegenerate_toMatrix₂'_iff, LinearMap.BilinForm.toMatrix'_comp, Module.equiv_free_prod_directSum, TensorProduct.equivFinsuppOfBasisRight_apply, WittVector.StandardOneDimIsocrystal.frobenius_apply, LinearEquiv.dualMap_apply, LinearEquiv.nonempty_equiv_iff_lift_rank_eq, LinearEquiv.funUnique_apply, TensorProduct.directSum_symm_lof_tmul, LinearEquiv.sumArrowLequivProdArrow_apply_fst, Rep.coindResAdjunction_homEquiv_symm_apply, LinearEquiv.coe_zero, Matrix.toLinearMapRight'_apply, LinearMap.BilinForm.toMatrix_mul, Finsupp.lcongr_single, LinearEquiv.submoduleMap_symm_apply, LinearMap.GeneralLinearGroup.coe_toLinearEquiv, LinearEquiv.canLiftContinuousLinearEquiv, Matrix.ofLp_toEuclideanLin_apply, Matrix.toLinearMap₂_apply, Finsupp.linearEquivFunOnFinite_apply, linearEquiv_det_rotation, ZLattice.abs_repr_lt_of_norm_lt, Complex.coe_selfAdjointEquiv, MultilinearMap.freeDFinsuppEquiv_apply, Rep.coindVEquiv_apply_hom, Polynomial.degreeLT.addLinearEquiv_symm_apply', LieAlgebra.LoopAlgebra.residuePairing_apply_apply, LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul, LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero, MvPolynomial.rTensor_apply_monomial_tmul, CoalgEquiv.coe_symm_toLinearEquiv, Algebra.Generators.repr_CotangentSpaceMap, LinearEquiv.congrQuadraticMap_symm_apply, Module.Basis.dualBasis_repr, PiTensorProduct.tmulEquiv_apply, BialgEquiv.trans_symm_apply, lieEquivMatrix'_symm_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr, Matrix.proj_diagonal, Module.Dual.baseChange_baseChange, LinearEquiv.prodCongr_apply, NumberField.mixedEmbedding.stdBasis_apply_isReal, ZMod.completedLFunction_one_sub_odd, LinearMap.isUnit_toMatrix_iff, Module.Basis.linearCombination_repr, TensorProduct.enorm_assoc, union_support_maximal_linearIndependent_eq_range_basis, MultilinearMap.curryMidLinearEquiv_apply, LinearMap.BilinForm.toMatrix_compLeft, LinearMap.trace_eq_matrix_trace, TensorProduct.quotientTensorEquiv_apply_tmul_mk, RootPairing.polarizationEquiv_symm_apply_coroot, BilinForm.toMatrix_apply, WeakDual.CharacterSpace.norm_le_norm_one, Pretrivialization.linearEquivAt_apply, Matrix.linfty_opNorm_toMatrix, exteriorPower.zeroEquiv_ιMulti, LinearEquiv.transvection.coe_apply, Matrix.toBilin'_apply', Matrix.toLinearMap₂'_single, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply, LinearMap.separatingRight_toLinearMap₂'_of_det_ne_zero', LinearMap.adjoint_inner_left, LinearEquiv.piCurry_symm_apply, Polynomial.eval_eq_sum_degreeLTEquiv, LinearMap.BilinForm.mul_toMatrix, Module.Basis.tensorAlgebra_repr_apply, LinearEquiv.symmEquiv_apply_symm_apply, TensorProduct.rightComm_tmul, LinearMap.coprodEquiv_apply, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, Module.Basis.equivFun_apply, Module.apply_evalEquiv_symm_apply, TensorProduct.finsuppScalarLeft_apply_tmul, TensorProduct.directSumRight_tmul, TensorProduct.gradedComm_tmul_algebraMap, LinearMap.trace_conj', Matrix.SpecialLinearGroup.toLin'_to_linearMap, ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv, Module.Basis.smulTower'_repr, TensorProduct.congr_mul, TensorProduct.norm_lid, LinearMap.mul_toMatrix₂'_mul, LinearMap.toMatrix₂'_mul, CliffordAlgebra.reverseEquiv_symm_apply, WithLp.linearEquiv_apply, LinearEquiv.ofSubmodule'_apply, Finsupp.LinearEquiv.finsuppUnique_apply, ZLattice.volume_image_eq_volume_div_covolume', Algebra.toMatrix_lsmul, LinearEquiv.rTensor_trans_apply, toMatrix_innerSL_apply, Module.Basis.map_orientation_eq_det_inv_smul, Matrix.separatingLeft_toLinearMap₂'_iff, LinearEquiv.inv_mem_dilatransvections_iff, exteriorPower.basis_repr_apply, Finsupp.linearEquivFunOnFinite_symm_single, LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero', TensorProduct.rid_symm_apply, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply, Module.Basis.toMatrix_update, TensorPower.cast_tprod, PiLp.basis_toMatrix_basisFun_mul, Submodule.mk_quotientEquivOfIsCompl_apply, Submodule.prodEquivOfIsCompl_symm_apply_right, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, BilinForm.toMatrix_mul, Rep.leftRegularHomEquiv_symm_single, LinearMap.toMatrix_comp, Module.reflection_mul_reflection_zpow_apply_self, Finsupp.mapRange.linearEquiv_apply, LocallyConstant.congrLeftₗ_apply_apply, SameRay.sameRay_map_iff, RootPairing.coreflection_apply, PositiveLinearMap.ofPreGNS_toPreGNS, Matrix.separatingLeft_toBilin'_iff, Module.Basis.baseChange_repr_tmul, TensorProduct.nnnorm_assoc, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply, Matrix.kroneckerAlgEquiv_symm_apply, Matrix.trace_toLin_eq, TensorPower.cast_eq_cast, LinearMap.toMatrix₂_mul_basis_toMatrix, ZSpan.repr_fract_apply, finsuppLEquivDirectSum_apply, LinearEquiv.ofTop_symm_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, KaehlerDifferential.quotKerTotalEquiv_symm_apply, LinearMap.quotKerEquivOfSurjective_symm_apply, finsuppTensorFinsuppLid_apply_apply, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul, LinearEquiv.smulOfNeZero_symm_apply, LinearEquiv.refl_apply, PiTensorProduct.lift_tprod, Matrix.toLinOfInv_apply, LinearEquiv.apply_symm_apply, dualTensorHomEquivOfBasis_symm_cancel_left, LinearEquiv.trans_smul, Module.Invertible.rTensorEquiv_symm_apply_apply, Complex.selfAdjointEquiv_symm_apply, QuaternionAlgebra.coe_basisOneIJK_repr, QuadraticMap.IsometryEquiv.coe_toLinearEquiv, RootPairing.Equiv.weightHom_injective, LinearEquiv.congr_arg, PiTensorProduct.liftIsometry_apply_apply, TensorProduct.AlgebraTensorModule.congr_one, ContinuousLinearEquiv.toLinearEquiv_injective, LinearEquiv.conj_id, DFinsupp.linearEquivFunOnFintype_apply, AddEquiv.coe_symm_toNatLinearEquiv, finsuppLequivDFinsupp_apply_apply, TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul, Submodule.FG.lTensor.directLimit_apply, Matrix.toBilin'Aux_eq, TensorProduct.lift.equiv_symm_apply, addMonoidHomLequivNat_apply, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix', Matrix.toLin_finTwoProd_toContinuousLinearMap, Orientation.volumeForm_zero_neg, CategoryTheory.Linear.homCongr_symm_apply, ZMod.dft_const_mul, TensorPower.one_mul, Finsupp.domLCongr_apply, RootPairing.isFixedPt_reflection_of_isOrthogonal, LinearMap.linearEquivOfInjective_apply, PiTensorProduct.norm_eval_le_projectiveSeminorm, LinearEquiv.toFun_eq_coe, AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_apply, LinearEquiv.conjRingEquiv_symm_apply_apply, Finsupp.curryLinearEquiv_apply, TensorProduct.map_map_assoc, Matrix.uniqueLinearEquiv_symm_apply, Module.reflection_mul_reflection_zpow_apply, LinearEquiv.sumArrowLequivProdArrow_apply_snd, Submodule.quotEquivOfEq_mk, RingEquiv.toSemilinearEquiv_apply, TensorProduct.commIsometry_apply, finsuppTensorFinsupp_symm_single, Polynomial.det_taylorLinearEquiv, addMonoidHomLequivInt_symm_apply, LinearEquiv.congr_fun, Matrix.toLinearEquivRight'OfInv_apply, hasEigenvalue_toLin'_diagonal_iff, LinearEquiv.map_smul, LinearEquiv.smul_id_of_finrank_eq_one_apply, LinearMap.toMatrix'_toLinearMapₛₗ₂', LinearMap.isStarProjection_toContinuousLinearMap_iff, LinearMap.linearEquiv_of_ne_zero, Rep.MonoidalClosed.linearHomEquiv_hom, Matrix.toLpLin_mul, Matrix.toLin'_submatrix, Derivation.compAEval_eq, Matrix.separatingLeft_toLinearMap₂_iff, LinearMap.ringLmapEquivSelf_apply, Matrix.toLin_toMatrix, PiTensorProduct.lift_comp_map, NumberField.mixedEmbedding.latticeBasis_repr_apply, Submodule.lTensorOne_symm_apply, LinearMap.toMatrix₂_apply, AdicCompletion.sumEquivOfFintype_apply, LinearEquiv.smul_def, Module.Basis.ext_elem_iff, AddEquiv.coe_toIntLinearEquiv, LinearMap.adjoint_comp, RootPairing.Equiv.weightEquiv_symm_weightMap, KaehlerDifferential.mvPolynomialBasis_repr_D, QuadraticForm.tensorAssoc_apply, RootPairing.coroot'_reflection, LinearMap.toContPerfPair_apply, Matrix.toEuclideanLin_apply_piLp_toLp, Module.AEval.of_aeval_smul, multilinearCurryLeftEquiv_symm_apply, Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply, finsuppTensorFinsuppRid_apply_apply, Module.Basis.repr_sum_self, LinearEquiv.piFinTwo_apply, Function.Exact.linearEquivOfSurjective_apply, RootPairing.Base.toWeightBasis_repr_root, MultilinearMap.coe_currySumEquiv, Algebra.leftMulMatrix_mulVec_repr, iSupIndep_iff_dfinsupp_lsum_injective, RootPairing.toPerfPair_conj_reflection, LinearEquiv.ofSubsingleton_symm_apply, Finsupp.supportedEquivFinsupp_symm_apply_coe, LinearEquiv.toSpanNonzeroSingleton_one, Module.Basis.parallelepiped_map, LinearMap.coe_quotientInfToSupQuotient, Module.Basis.smulTower_repr_mk, Module.Basis.repr_support_subset_of_mem_span, LinearEquiv.prodAssoc_apply, MultilinearMap.curryMidLinearEquiv_symm_apply, Polynomial.toMatrix_sylvesterMap, Finsupp.supportedEquivFinsupp_apply_support_val, finsuppLequivDFinsupp_symm_apply, Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply, Finsupp.lsum_comp_lsingle, TensorProduct.finsuppRight_symm_apply_single, TensorProduct.gradedComm_one_tmul, Matrix.separatingRight_toBilin'_iff, Trivialization.coe_coordChangeL, CoalgEquiv.trans_symm_apply, TensorProduct.prodRight_tmul, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, Matrix.toLin_finTwoProd, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap, LinearMap.BilinForm.apply_toDual_symm_apply, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, Module.Basis.linearMap_repr_symm_apply, Module.Basis.constr_basis, IsBaseChange.equiv_tmul, LinearEquiv.charpoly_conj, ModuleCat.homLinearEquiv_apply, Algebra.Generators.snd_cotangentCompLocalizationAwayEquiv, SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply, QuaternionAlgebra.coe_linearEquivTuple, finsuppTensorFinsuppLid_single_tmul_single, LinearEquiv.nonempty_equiv_iff_rank_eq, LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl, Matrix.kroneckerTMulAlgEquiv_apply, RootPairing.reflection_inv, ZSpan.map_fundamentalDomain, LinearMap.nondegenerate_toMatrix₂_iff, LieEquiv.toLinearEquiv_injective, AlgEquiv.linearEquivConj_mulRight, ModuleCat.Iso.conj_eq_conj, MeasureTheory.Measure.addHaar_preimage_linearEquiv, Matrix.toLin_one, TensorAlgebra.mk_reindex_fin_cast, CliffordAlgebra.reverseEquiv_apply, Matrix.toLin_transpose, GradedTensorProduct.of_symm_of, SemilinearEquivClass.semilinearEquiv_apply, linearEquivIsoModuleIso_inv, Complex.toMatrix_conjAe, BilinForm.mul_toMatrix, Matrix.toLpLin_symm_comp, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, Matrix.toLinearMapₛₗ₂_apply_basis, Module.Ray.map_apply, TensorProduct.tensorTensorTensorAssoc_symm_tmul, TensorProduct.finsuppLeft_apply_tmul, LinearEquiv.coord_apply_smul, PiTensorProduct.ofFinsuppEquiv'_apply_apply, LinearMap.toMatrix_toSpanSingleton, LinearEquiv.coe_inv_det, RootPairing.toPerfPair_flip_conj_coreflection, Polynomial.degreeLT.addLinearEquiv_natAdd, TensorProduct.lidOfCompatibleSMul_tmul, Coalgebra.coassoc_apply, ZMod.invDFT_def, LinearMap.GeneralLinearGroup.toLinearEquiv_mul, LinearEquiv.coe_toLinearMap, MulOpposite.coe_opLinearEquiv, Representation.coinvariantsFinsuppLEquiv_symm_apply, LinearMap.Nondegenerate.toMatrix₂', RootPairing.Equiv.reflection_smul, Subalgebra.linearEquivOp_symm_apply_coe, TensorProduct.equivFinsuppOfBasisRight_symm, CategoryTheory.Abelian.Ext.mk₀_linearEquiv₀_apply, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, exteriorPower.basis_repr, LinearEquiv.lTensor_trans_apply, Submodule.lTensorOne_tmul, instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId, Matrix.Nondegenerate.toBilin', FDRep.Iso.conj_ρ, TensorProduct.directLimitLeft_tmul_of, ContinuousLinearMap.toSpanSingletonLE_symm_apply, LinearMap.toMatrix_singleton, LinearMap.BilinForm.toMatrix'_mul, Submodule.LinearDisjoint.val_mulMap_tmul, LinearEquiv.transvection.inv_eq', AddEquiv.coe_toNatLinearEquiv, Algebra.traceMatrix_of_basis_mulVec, IsBaseChange.basis_repr_comp, exteriorPower.alternatingMapLinearEquiv_symm_apply, OrthonormalBasis.coe_toBasis_repr_apply, TensorProduct.lid'_symm_apply, ZLattice.normBound_spec, LinearMap.toMatrix₂'_compl₂, PiTensorProduct.map_reindex, TensorPower.mul_algebraMap₀, Rep.leftRegularHomEquiv_apply, LinearEquiv.ext_iff, Function.Exact.linearEquivOfSurjective_symm_apply, LinearEquiv.coe_injective, 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, PiTensorProduct.lift.unique', Matrix.nondegenerate_toLinearMap₂'_iff, LinearMap.separatingRight_toMatrix₂_iff, DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne, Matrix.SpecialLinearGroup.toLin'_injective, TensorProduct.piScalarRight_apply, NumberField.Units.logEmbeddingEquiv_apply, RootPairing.coreflection_same, LinearEquiv.lTensor_symm_tmul, Module.Invertible.linearEquivOfRightInverse_apply, SpecialLinearGroup.coe_toGeneralLinearGroup_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis, LinearEquiv.baseChange_pow, Module.Basis.ofZLatticeComap_repr_apply, starLinearEquiv_apply, AlternatingMap.domDomCongrₗ_symm_apply, TensorProduct.directLimitLeft_symm_of_tmul, LinearIsometryEquiv.norm_map', LinearMap.toMvPolynomial_eval_eq_apply, LinearEquiv.coe_one, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, Module.Basis.toMatrix_transpose_apply, nonempty_linearEquiv_of_lift_rank_eq, LinearEquiv.coe_ofTop_symm_apply, LinearMap.separatingLeft_toMatrix₂_iff, ContinuousLinearMap.toUniformConvergenceCLM_continuous, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, TensorProduct.comm_tmul, Representation.asModuleEquiv_map_smul, Submodule.fstEquiv_symm_apply_coe, AdicCompletion.piEquivOfFintype_apply, Module.Basis.ofZLatticeBasis_repr_apply, LinearEquiv.neg_apply, fromModuleCatToModuleCatLinearEquiv_apply, DirectSum.linearEquivFunOnFintype_symm_single, LinearMap.BilinForm.toMatrix'_toBilin', LinearEquiv.symm_smul_apply, IsIsotypic.linearEquiv_finsupp, fromModuleCatToModuleCatLinearEquiv_symm_apply_coe, PowerBasis.liftEquiv'_symm_apply_apply, PiTensorProduct.lift_comp_reindex_symm, PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod, LinearEquiv.coe_toEquiv_symm, PowerBasis.constr_pow_mul, StrongDual.coe_toWeakDual, LinearMap.det_toMatrix', LinearMap.GeneralLinearGroup.ofLinearEquiv_mul, Matrix.separatingLeft_toBilin_iff, TensorProduct.congr_pow, WeakDual.toStrongDual_apply, LinearMap.eq_adjoint_iff_basis_right, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, 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, MultilinearMap.constLinearEquivOfIsEmpty_symm_apply, toWeakSpaceCLM_eq_toWeakSpace, TensorProduct.equivFinsuppOfBasisLeft_apply, Module.Basis.prod_repr_inr, LinearEquiv.pow_apply, LinearEquiv.symmEquiv_symm_apply_symm_apply, LinearMap.BilinForm.Nondegenerate.toMatrix', AlternatingMap.domLCongr_apply, Module.Basis.constr_self, Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inl, LinearMap.toMatrix_basis_equiv, Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inr, Matrix.reindexLinearEquiv_comp_apply, LinearEquiv.toAddEquiv_toNatLinearEquiv, CategoryTheory.Abelian.Ext.linearEquiv₀_symm_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, Matrix.SeparatingRight.toBilin', Matrix.kroneckerTMul_assoc, LinearEquiv.injective, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, AdicCompletion.ofLinearEquiv_apply, AffineIsometryEquiv.norm_map, Rep.diagonalHomEquiv_apply, LinearMap.coe_toContinuousLinearMap_symm, Matrix.range_diagonal, ZMod.completedLFunction_one_sub_even, Matrix.piLinearEquiv_symm_apply, LinearMap.extendScalarsOfIsLocalizationEquiv_symm_apply, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, Module.reflection_apply, Module.Basis.constr_def, Rep.freeLiftLEquiv_symm_apply, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply, BilinForm.toMatrix_compLeft, LinearMap.IsPositive.adjoint_eq, Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace, ContinuousLinearMap.prodₗ_apply, ContinuousLinearMap.coprodEquiv_symm_apply, AdicCompletion.congr_apply, Module.Basis.toDual_apply_left, LinearMap.toPerfPair_apply, LinearMap.equivOfIsUnitDet_apply, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, LinearMap.toMatrix₂'_comp, MvPolynomial.rTensor_apply, LinearEquiv.congrQuadraticMap_apply, RootPairing.IsOrthogonal.coreflection_apply_left, Matrix.toLinearMap₂_apply_basis, LinearEquiv.conjAlgEquiv_surjective, LinearEquiv.smul_trans, Matrix.coe_ofLinearEquiv_symm, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, LinearMap.toMatrix_pow, IsBaseChange.linearMapLeftRightHom_apply, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply, LinearMap.coprodEquiv_symm_apply, LinearMap.BilinForm.toMatrix_comp, LinearEquiv.map_mem_invtSubmodule_iff, LinearMap.mul'_comm, Matrix.SpecialLinearGroup.toLin'_symm_apply, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, Module.Basis.reindexFinsetRange_repr, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, Module.Basis.continuous_coe_repr, TensorProduct.finsuppScalarLeft_apply, Submodule.lTensorOne_one_tmul, Module.Basis.smulTower_repr, Module.Basis.toDual_apply_right, LinearMap.toMatrix'_one, AffineEquiv.map_vadd', AlternatingMap.domDomCongrₗ_apply, KaehlerDifferential.tensorKaehlerEquiv_tmul_D, Module.surjective_piEquiv_apply_iff, LinearMap.transvection.congr, ZSpan.repr_floor_apply, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, Rep.indResHomEquiv_apply_hom, LinearEquiv.automorphismGroup.toLinearMapMonoidHom_apply, Module.Basis.repr_symm_apply, Module.Dual.congr_apply_apply, PiTensorProduct.ofDirectSumEquiv_tprod_apply, LinearMap.tensorKerEquiv_apply, basis_toMatrix_mul_linearMap_toMatrix, LinearMap.toMatrixₛₗ₂'_apply, Submodule.mem_biSup_iff_exists_dfinsupp, LinearEquiv.one_eq_refl, Module.Basis.tensorProduct_repr_tmul_apply, Module.Basis.coe_ofEquivFun, PolynomialLaw.ground_apply, Matrix.toLinearMapRight'_one, LinearEquiv.ofLinear_symm_apply, Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace, LinearEquiv.coe_uniqueProd, LinearEquiv.alternatingMapCongrRight_symm_apply_apply, WithLp.linearEquiv_symm_apply, MultilinearMap.curryFinFinset_symm_apply, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift, LinearEquiv.lTensor_refl_apply, Basis.piTensorProduct_repr_tprod_apply, LinearEquiv.inv_mem_transvections_iff, Module.Basis.sum_equivFun, WithLp.coe_symm_linearEquiv, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, TensorProduct.finsuppScalarLeft_symm_apply_single, Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix, Module.Finite.exists_fin_quot_equiv, Submodule.comapSubtypeEquivOfLe_apply_coe, RootPairing.range_weylGroup_weightHom, Module.Basis.repr_smul', lmap_finsuppLEquivDirectSum_eq, LinearMap.lsum_piSingle, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, Algebra.TensorProduct.equivPiOfFiniteBasis_apply, Module.Basis.constr_range, Module.Basis.repr_unitsSMul, Module.compHom.toLinearEquiv_symm_apply, RootPairing.reflection_apply, TensorProduct.piRight_apply, Matrix.toLpLin_apply, TensorProduct.congrIsometry_apply, ZMod.dft_eq_fourier, LinearEquiv.baseChange_one, ZMod.dft_odd_iff, Matrix.toLin'_apply, LinearEquiv.det_refl, LinearEquiv.arrowCongr_comp, Module.Basis.constr_apply, LinearEquiv.piCongrLeft'_apply, DFinsupp.lsum_apply_apply, LinearMap.BilinForm.SeparatingRight.toMatrix', Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, ContinuousLinearMap.toUniformConvergenceCLM_symm_apply, Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero, Derivation.linearEquiv_coe_comp, Finsupp.linearCombination_eq_fintype_linearCombination_apply, LinearMap.toMatrix_adjoint, GradedTensorProduct.of_one, Matrix.compLinearEquiv_apply, Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, SpecialLinearGroup.baseChange_apply_coe, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, LinearEquiv.instSemilinearEquivClass, LinearEquiv.ofInjective_symm_apply, LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero, Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply, AddEquiv.coe_toLinearEquiv, CharacterModule.homEquiv_apply_apply, Submodule.mem_map_equiv, LinearMap.BilinForm.Nondegenerate.toMatrix, TensorProduct.nnnorm_lid, LinearMap.im_inner_adjoint_mul_self_eq_zero, AlgEquiv.toLinearEquiv_injective, TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk, LinearEquiv.coe_symm_mk', Matrix.l2_opNorm_def, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, exteriorPower.oneEquiv_ιMulti, GradedTensorProduct.symm_of_of, Matrix.toEuclideanLin_toLp, Module.Basis.repr_eq_iff', LinearMap.toLinearMap_toPerfPair, RootPairing.coroot_reflectionPerm, TensorProduct.gradedComm_of_tmul_of, PowerBasis.constr_pow_aeval, Submodule.map_equivMapOfInjective_symm_apply, Finsupp.supportedEquivFinsupp_symm_apply_coe_apply, LinearMap.det_toMatrix, Algebra.traceForm_toMatrix_powerBasis, Matrix.minpoly_toLin, basis_toMatrix_mul, SemimoduleCat.homLinearEquiv_symm_apply, Matrix.toLin'_toMatrix', ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply, LinearMap.det_toLin, Module.Basis.det_map, LieModule.shiftedGenWeightSpace.shift_symm_apply, LinearMap.posSemidef_toMatrix_iff, Representation.linHom.invariantsEquivRepHom_apply_hom, Matrix.coe_ofLinearEquiv, ZMod.LFunction_dft, Module.Basis.norm_repr_le_norm, LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero', LinearEquiv.smul_refl, MvPolynomial.scalarRTensor_apply_tmul_apply, Module.Basis.mem_span_repr_support, Derivation.compAEval_apply, Pi.basisFun_repr, Algebra.leftMulMatrix_eq_repr_mul, TensorProduct.directLimitRight_symm_of_tmul, FGModuleCat.Iso.conj_hom_eq_conj, Finsupp.finsuppProdLEquiv_symm_apply_apply, Module.Basis.toDual_eq_equivFun, LinearMap.SeparatingLeft.toMatrix₂', RootPairing.isOrthogonal_comm, TensorProduct.toMatrix_comm, Module.Basis.sum_repr, RootPairing.coreflection_apply_coroot, ZMod.dft_const_smul, RootPairing.Equiv.coweightHom_toLinearMap, Finsupp.supportedEquivFinsupp_apply_apply, SpecialLinearGroup.coe_div, 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, TensorProduct.assoc_symm_tmul, AdicCompletion.sumEquivOfFintype_symm_apply, Matrix.kroneckerStarAlgEquiv_apply, Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom, TensorProduct.comm_symm_tmul, LinearMap.BilinForm.separatingLeft_toMatrix_iff, TensorProduct.sum_tmul_basis_left_injective, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, exteriorPower.zeroEquiv_symm_apply, ZMod.dft_smul_const, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Module.torsion_by_prime_power_decomposition, Module.AEval.mem_mapSubmodule_apply, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, SpecialLinearGroup.toLinearEquiv_injective, PiTensorProduct.lift.unique, TensorProduct.equivFinsuppOfBasisRight_symm_apply, Real.volume_preserving_transvectionStruct, ContinuousAlternatingMap.piLinearEquiv_apply, ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT, Matrix.toLpLinAlgEquiv_symm_apply, RootPairing.Equiv.coweightHom_apply, Matrix.toBilin'_toMatrix', Module.Basis.algebraMapCoeffs_repr, Module.Invertible.linearEquivOfLeftInverse_apply, Submodule.sndEquiv_apply, LinearEquiv.multilinearMapCongrLeft_apply, LieEquiv.ofBijective_invFun, Submodule.sndEquiv_symm_apply_coe, Matrix.toLinearMapₛₗ₂_toMatrix₂, Submodule.comapSubtypeEquivOfLe_symm_apply, Module.Basis.coord_apply, LinearMap.toMatrix'_mulVec, LinearMap.lsum_symm_apply, Module.Basis.mem_span_iff_repr_mem, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range, IsBaseChange.toDualBaseChange_tmul, Matrix.SeparatingLeft.toLinearMap₂, KaehlerDifferential.quotKerTotalEquiv_apply, ULift.moduleEquiv_apply, hasEigenvector_toLin_diagonal, LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero, Module.Basis.coord_equivFun_symm, RootPairing.reflection_reflectionPerm, quotient_prod_linearEquiv, ZMod.dft_def, dotProduct_toMatrix₂_mulVec, TensorProduct.gradedComm_gradedMul, Matrix.diagonal_comp_single, Algebra.Generators.H1Cotangent.equiv_apply, LinearMap.toMatrixAlgEquiv_transpose_apply, LinearEquiv.rTensor_tmul, Submodule.Quotient.restrictScalarsEquiv_mk, Module.Basis.repr_self, AdicCompletion.piEquivFin_apply, NormedSpace.Dual.toWeakDual_inj, IsLocalizedModule.lift_iso, SpecialLinearGroup.coe_dualMap, TensorProduct.finsuppRight_apply_tmul_apply, Shrink.linearEquiv_apply, TensorProduct.directSumRight_symm_lof_tmul, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply, LinearEquiv.transvection.inv_eq, Polynomial.taylorLinearEquiv_apply_coe, LinearMap.traceAux_def, LinearEquiv.mem_transvections, MultilinearMap.fromDFinsuppEquiv_symm_apply, Algebra.leftMulMatrix_apply, PiTensorProduct.congr_tprod, AdicCompletion.ofLinearEquiv_symm_of, InnerProductSpace.symm_toEuclideanLin_rankOne, LinearMap.BilinForm.toMatrix'_compRight, TensorProduct.finsuppRight_apply_tmul, LinearEquiv.ofTop_apply, Module.subsingletonEquiv_apply, linearEquivIsoModuleIsoₛ_inv, Polynomial.degreeLT.basis_repr, nonempty_linearEquiv_of_rank_eq, Matrix.SeparatingRight.toBilin, Module.reflection_mul_reflection_mul_reflection_pow_apply_self, LieModule.coe_maxTrivLinearMapEquivLieModuleHom, Module.Basis.repr_reindex_apply, Module.reflection_mul_reflection_mul_reflection_zpow_apply_self, LinearEquiv.coe_toLinearMap_one, Module.reflection_mul_reflection_zpow, Matrix.transposeLinearEquiv_apply, LinearMap.toMatrix_apply, RootPairing.mapsTo_coreflection_coroot, NumberField.house.basis_repr_norm_le_const_mul_house, TensorProduct.toMatrix_map, Matrix.rank_vecMulVec, LinearMap.quotKerEquivOfSurjective_apply_mk, ContinuousLinearMap.toWOT_apply, LinearEquiv.lTensor_mul, Submodule.coe_prodEquivOfClosedCompl, LinearEquiv.coe_coe, Algebra.SubmersivePresentation.cotangentEquiv_apply, LinearMap.toMatrix_id_eq_basis_toMatrix, DirectSum.lequivProdDirectSum_symm_apply, LinearMap.toMatrixAlgEquiv_transpose_apply', TensorProduct.dualDistribEquivOfBasis_apply_apply, RootPairing.root_reflectionPerm, LinearMap.toMatrixRight'_comp, LinearEquiv.ofLinear_apply, PositiveLinearMap.preGNS_norm_sq, Matrix.kroneckerStarAlgEquiv_symm_apply, Submodule.coe_equivMapOfInjective_apply, Module.dualProdDualEquivDual_symm_apply, TensorProduct.assocIsometry_symm_apply, Module.Basis.constr_eq, Fin.consLinearEquiv_symm_apply, Finsupp.domLCongr_single, SpecialLinearGroup.toLinearEquiv_to_linearMap, LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm, Complex.nonempty_linearEquiv_real, Matrix.toBilin_comp, LinearEquiv.apply_ofBijective_symm_apply, TensorProduct.coe_finsuppScalarRight', LinearMap.polyCharpoly_coeff_eval, ContinuousLinearEquiv.coe_symm_toLinearEquiv, 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, DirectSum.linearEquivFunOnFintype_apply, MultilinearMap.ofSubsingletonₗ_symm_apply, LinearMap.det_toMatrix_eq_det_toMatrix, LinearEquiv.toAddEquiv_toIntLinearEquiv, LinearEquiv.coe_addEquiv_apply, Algebra.TensorProduct.linearEquivIncludeRange_tmul, Matrix.SpecialLinearGroup.toLin'_apply, TensorProduct.AlgebraTensorModule.congr_tmul, Submodule.piQuotientLift_mk, LinearMap.adjoint_id, MultilinearMap.currySumEquiv_symm_apply, exteriorPower.basis_repr_self, TensorProduct.finsuppLeft'_apply, GradedTensorProduct.of_symm_one, LinearMap.lflip_apply, Submodule.coe_prodEquivOfClosedCompl_symm, TensorProduct.lift.equiv_apply, TensorProduct.finsuppRight_tmul_single, Rep.indResHomEquiv_symm_apply_hom, QuadraticForm.dualProdProdIsometry_invFun, LinearMap.SeparatingLeft.congr, Int.submodule_toAddSubgroup_index_ne_zero_iff, Submodule.fstEquiv_apply, Matrix.Nondegenerate.toLinearMap₂', finsuppLEquivDirectSum_symm_lof, LinearEquiv.extendScalarsOfIsLocalization_apply, Trivialization.linearEquivAt_symm_apply, Finsupp.curryLinearEquiv_symm_apply, LinearEquiv.coe_det, Matrix.separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂, Module.Basis.sumQuot_repr_inr, Module.Basis.coord_toDualEquiv_symm_apply, Finsupp.lsum_symm_apply, Module.Basis.coord_repr_symm, ZMod.dft_apply_zero, Finsupp.lcongr_apply_apply, StarModule.decomposeProdAdjoint_apply, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul, LinearEquiv.skewProd_apply, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, Subspace.dualEquivDual_apply, Ideal.isoBaseOfIsPrincipal_apply, LinearEquiv.prodUnique_apply, ZLattice.abs_repr_le, Module.Dual.congr_symm_apply_apply, DirectSum.IsInternal.collectedBasis_repr_of_mem, Module.Basis.coe_sumCoords, Submodule.restrictScalarsEquiv_apply, coe_ofLexLinearEquiv, RootPairing.reflection_image_eq, DirectSum.coe_congrLinearEquiv, RootPairing.Equiv.coweightEquiv_apply, DirectSum.lequivProdDirectSum_apply, LinearMap.sum_repr_mul_repr_mul, LinearMap.IsPositive.conj_adjoint, Fin.consLinearEquiv_apply, LinearMap.ker_toContinuousLinearMap, IsLocalizedModule.iso_mk_one, LinearMap.charpoly_toMatrix, LinearMap.isSymm_iff_isHermitian_toMatrix, Module.Basis.ofIsLocalizedModule_repr_apply, LinearEquiv.apply_faithfulSMul, DFinsupp.domLCongr_apply, Matrix.toBilin'_single, Submodule.Quotient.equiv_apply, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply, LinearEquiv.conjAlgEquiv_ext_iff, LinearMap.toMatrix_toLin, TensorProduct.includeRight_lid, LieEquiv.coe_toLinearEquiv, TensorProduct.tensorTensorTensorAssoc_tmul, AddEquiv.coe_symm_toIntLinearEquiv, TensorProduct.finsuppLeft_apply_tmul_apply, Module.compHom.toLinearEquiv_apply, IsNoetherian.equivPUnitOfProdInjective_symm_apply, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, SpecialLinearGroup.toLinearEquiv_apply, Matrix.toLinearEquiv_apply, LinearEquiv.piRing_apply, hasEigenvalue_toLin_diagonal_iff, PiTensorProduct.lift_symm, LinearEquiv.prodProdProdComm_toAddEquiv, sigmaFinsuppLequivDFinsupp_apply, RootPairing.reflection_apply_root, Matrix.spectrum_toLin', kroneckerLinearEquiv_tmul, AlgEquiv.toLinearEquiv_apply, MvPolynomial.rTensorAlgHom_apply_eq
LinearEquivClass 📖	MathDef	5 math math: AlgEquivClass.toLinearEquivClass, RingEquivClass.toLinearEquivClassRat, QuadraticMap.IsometryEquiv.instLinearEquivClass, LieModuleEquiv.instLinearEquivClass, LieEquiv.instLinearEquivClass
SemilinearEquivClass 📖	CompData	4 math math: SemilinearIsometryEquivClass.toSemilinearEquivClass, CoalgEquivClass.toSemilinearEquivClass, LinearEquiv.instSemilinearEquivClass, ContinuousSemilinearEquivClass.toSemilinearEquivClass
«term_≃ₗ[_]_» 📖	CompOp	—
«term_≃ₛₗ[_]_» 📖	CompOp	—

---

← Back to Index