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, symm_toSemilinearEquiv_symm_apply, toSemilinearEquiv_apply, toSemilinearEquiv_symm_apply, instSemilinearMapClass, map_smulₛₗ, semilinearEquiv_apply, toAddEquivClass	103
Total	127

LinearEquiv

Definitions

Name	Category	Theorems
cast 📖	CompOp	2 math math: cast_symm_apply, cast_apply
instCoeLinearMap 📖	CompOp	—
instEquivLike 📖	CompOp	855 math math: multilinearMapCongrLeft_symm_apply, MultilinearMap.domDomCongrLinearEquiv'_symm_apply, continuous_decomposeProdAdjoint, LieModule.shiftedGenWeightSpace.shift_apply, TensorProduct.AlgebraTensorModule.distribBaseChange_symm_tmul, Finsupp.snd_sumFinsuppLEquivProdFinsupp, coe_toEquiv, IsLocalizedModule.iso_symm_apply', Finsupp.fst_sumFinsuppLEquivProdFinsupp, Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, AddMonoidAlgebra.supportedEquivFinsupp_apply_apply, 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, 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, ContinuousAffineMap.fst_decompLinearEquiv, 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, mk_coe', PiTensorProduct.map_reindex_symm, WithLp.coe_linearEquiv, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply, 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, Module.Dual.extendRCLikeₗ_symm_apply, 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, TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_symm_apply_mk_tmul, 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', AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val, 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, 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, Unitization.linearEquiv_symm_apply, eq_symm_apply, LinearMap.BilinForm.congr_comp, TensorProduct.quotTensorEquivQuotSMul_mk_one_tmul, Finsupp.LinearEquiv.finsuppUnique_symm_apply, MultilinearMap.domDomCongrLinearEquiv_symm_apply, AddEquiv.toNatLinearEquiv_toAddEquiv, coe_curry, PositiveLinearMap.leftMulMapPreGNS_apply, image_symm_eq_preimage, AffineEquiv.congrLeftₗ_symm_apply, 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, ContinuousAffineMap.decompLinearEquiv_symm_contLinear, 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, NormedSpace.inclusionInDoubleDualWeak_apply_apply, Matrix.piLinearEquiv_apply, baseChange_symm_tmul, PiTensorProduct.congr_symm_tprod, ExteriorAlgebra.liftAlternatingEquiv_apply, coe_pow, TensorProduct.prodLeft_tmul, ofLeftInverse_symm_apply, isOpenMap_toWeakSpace_symm, KaehlerDifferential.linearMapEquivDerivation_apply_apply, lp.zeroBasis_repr_apply, comp_symm_eq, Submodule.botEquivPUnit_symm_apply, TensorProduct.map_map_assoc_symm, Module.Basis.addSubgroupOfClosure_repr_apply, KaehlerDifferential.tensorKaehlerEquivBase_symm_apply, Module.Basis.span_repr_eq_single, 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, Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl, AffineEquiv.map_vadd, Module.Basis.repr_linearCombination, TensorProduct.assoc_tmul, PiTensorProduct.reindex_tprod, Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply, WithConv.congrLinearEquiv_apply, LinearMap.prodEquiv_symm_apply, extendScalarsOfSurjective_apply, LinearIndependent.linearCombinationEquiv_apply_coe, TensorProduct.AlgebraTensorModule.leftComm_tmul, ModularGroup.lcRow0Extend_apply, Units.mulRightLinearEquiv_mul_apply, IsTensorProduct.assocOfMapSMul_symm_tmul, 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, MonoidAlgebra.coeffLinearEquiv_symm_apply, Module.Basis.equiv'_symm_apply, Module.Basis.repr_reindex, TensorProduct.lid_tmul, Module.subsingletonEquiv_symm_apply, extendScalarsOfIsLocalization_symm_apply, IsTensorProduct.assoc_symm_tmul, 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, AffineEquiv.arrowCongrₗ_symm_apply, Submodule.comap_equiv_self_of_inj_of_le_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, StrongDual.extendRCLikeₗ_apply, Module.Basis.singleton_repr, TensorProduct.map_comm, NormedSpace.inclusionInDoubleDualWeak_apply, toSpanNonzeroSingleton_apply, ContinuousLinearEquiv.coe_toLinearEquiv, DFinsupp.linearEquivFunOnFintype_symm_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, arrowCongr_apply, finTwoArrow_apply, Submodule.prodEquivOfIsCompl_symm_apply, skewProd_symm_apply, Representation.linHom.invariantsEquivRepHom_apply, Submodule.Quotient.restrictScalarsEquiv_symm_mk, Matrix.liftLinear_apply, PiTensorProduct.lift_comp_reindex, PiTensorProduct.dualDistribEquivOfBasis_apply_apply, Rep.resCoindHomEquiv_symm_apply, conjRingEquiv_apply_apply, Module.Basis.toDual_eq_repr, TensorProduct.lid'_apply_tmul, Module.Basis.sum_repr_mul_repr, AlgEquiv.ofLinearEquiv_apply, symm_trans_apply, Module.Basis.linearMap_repr_apply, AddMonoidAlgebra.coeffLinearEquiv_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, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, LinearIsometryEquiv.withLpProdCongr_symm_apply, conj_symm_conj, Bundle.Pretrivialization.linearEquivAt_symm_apply, coe_curry_symm, Submodule.range_lsum_smul, 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, Rep.coindVEquiv_apply, Module.Dual.extendRCLikeₗ_apply, 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, Submodule.smul_top_eq_range_lsum, 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, StrongDual.extendRCLikeₗ_symm_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, MonoidAlgebra.coeffLinearEquiv_apply, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, 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, IsTensorProduct.assoc_tmul, sigmaFinsuppLequivDFinsupp_symm_apply, TensorProduct.leftComm_symm_tmul, ofLeftInverse_apply, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, RingEquiv.toSemilinearEquiv_symm_apply, MonoidAlgebra.supportedEquivFinsupp_apply_support_val, coe_ofInvolutive, symmEquiv_symm_apply_apply, SemimoduleCat.Iso.conj_eq_conj, Module.Basis.coe_ofRepr, dualMap_apply, symm_mk, funUnique_apply, sumArrowLequivProdArrow_apply_fst, coe_zero, IsTensorProduct.assocOfMapSMul_tmul, WithAbs.linearEquiv_symm_apply, Finsupp.lcongr_single, submoduleMap_symm_apply, LinearMap.GeneralLinearGroup.coe_toLinearEquiv, AffineEquiv.arrowCongrₗ_apply, Finsupp.linearEquivFunOnFinite_apply, Units.symm_mulLeftLinearEquiv_apply, MonoidAlgebra.supportedEquivFinsupp_apply_apply, toSpanNonzeroSingleton_symm_apply_smul, congrQuadraticMap_symm_apply, Module.Basis.dualBasis_repr, PiTensorProduct.tmulEquiv_apply, BialgEquiv.trans_symm_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr, prodCongr_apply, AddMonoidAlgebra.coeffLinearEquiv_symm_apply, Module.Basis.linearCombination_repr, union_support_maximal_linearIndependent_eq_range_basis, MultilinearMap.curryMidLinearEquiv_apply, TensorProduct.quotientTensorEquiv_apply_tmul_mk, 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, Rep.indResHomEquiv_apply, 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, Rep.resCoindHomEquiv_apply, 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, ContinuousAffineMap.decompLinearEquiv_symm_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, RingEquiv.symm_toSemilinearEquiv_symm_apply, smul_def, Module.Basis.ext_elem_iff, AddEquiv.coe_toIntLinearEquiv, TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_apply_tmul, LinearMap.toContPerfPair_apply, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_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, WithAbs.linearEquiv_apply, AlgEquiv.linearEquivConj_mulRight, ModuleCat.Iso.conj_eq_conj, Bundle.Pretrivialization.linearEquivAt_apply, Units.mulLeftLinearEquiv_mul_apply, 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, AddEquiv.linearEquiv_symm_apply, Subalgebra.linearEquivOp_symm_apply_coe, CategoryTheory.Abelian.Ext.mk₀_linearEquiv₀_apply, lTensor_trans_apply, WithConv.symm_congrLinearEquiv_apply, isUniformEmbedding, ContinuousLinearMap.toSpanSingletonLE_symm_apply, AddEquiv.coe_toNatLinearEquiv, TensorProduct.lid'_symm_apply, PiTensorProduct.map_reindex, ext_iff, Function.Exact.linearEquivOfSurjective_symm_apply, Unitization.linearEquiv_apply, coe_injective, PiTensorProduct.lift.unique', TensorProduct.piScalarRight_apply, lTensor_symm_tmul, starLinearEquiv_apply, AlternatingMap.domDomCongrₗ_symm_apply, Rep.indResHomEquiv_symm_apply, Units.symm_mulRightLinearEquiv_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, lp.zeroBasis_repr_symm_apply_coe, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, Matrix.toLin'OfInv_apply, ContinuousAffineMap.snd_decompLinearEquiv, 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, 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, Module.Basis.repr_symm_apply, Module.Dual.congr_apply_apply, Module.Basis.coe_ofEquivFun, Representation.freeLiftLEquiv_symm_apply, 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, Representation.leftRegularMapEquiv_apply, instSemilinearEquivClass, ofInjective_symm_apply, Representation.Equiv.dualTensorHom_invFun, 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, Matrix.coe_ofLinearEquiv, Representation.freeLiftLEquiv_apply, Module.Basis.mem_span_repr_support, Finsupp.finsuppProdLEquiv_symm_apply_apply, Module.Basis.toDual_eq_equivFun, Module.Basis.sum_repr, Finsupp.supportedEquivFinsupp_apply_apply, Submodule.image_smul_top_eq_range_lsum, 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, TensorProduct.AlgebraTensorModule.distribBaseChange_tmul, LinearMap.lsum_symm_apply, Module.Basis.mem_span_iff_repr_mem, KaehlerDifferential.quotKerTotalEquiv_apply, ULift.moduleEquiv_apply, Units.mulLeftLinearEquiv_apply, Units.mulRightLinearEquiv_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, AffineEquiv.congrLeftₗ_apply, 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, 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, AddEquiv.linearEquiv_apply, LinearMap.sum_repr_mul_repr_mul, Fin.consLinearEquiv_apply, IsLocalizedModule.iso_mk_one, Module.Basis.ofIsLocalizedModule_repr_apply, Representation.leftRegularMapEquiv_symm_apply_toFun, 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	78 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, fixedReduce_eq_one, Module.Basis.equiv_refl, refl_mem_transvections, ModularGroup.lcRow0Extend_symm_apply, Module.Invertible.tensorProductComm_eq_refl, fixedSubmodule_eq_top_iff, 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, Submodule.Quotient.equiv_refl, 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	16 math math: coe_toAddEquiv, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, Finsupp.mapRange.linearEquiv_toAddEquiv, DirectSum.congr_linearEquiv_toAddEquiv, WithLp.toAddEquiv_linearEquiv, QuadraticForm.dualProdIsometry_invFun, Unitization.toAddEquiv_linearEquiv, 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	14 math math: coe_toEquiv, coe_symm_toEquiv, FirstOrder.Field.lift_genericMonicPoly, Units.toEquiv_mulLeftLinearEquiv, ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv, toEquiv_inj, toEquiv_symm, LinearIndependent.linearCombinationEquiv_symm_apply, WithConv.toEquiv_congrLinearEquiv, toEquiv_injective, ContinuousLinearEquiv.coe_uniqueProd, ContinuousLinearEquiv.coe_prodUnique, coe_toEquiv_symm, Units.toEquiv_mulRightLinearEquiv
toLinearMap 📖	CompOp	522 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, Unitary.toLinearMap_mulRight, Submodule.comap_equiv_eq_map_symm, GradedTensorProduct.hom_ext_iff, coe_toLinearMap_flip, coe_baseChange, RootPairing.Base.forall_mem_support_invtSubmodule_iff, ker_le_fixedSubmodule_transvection, Units.toLinearMap_mulRightLinearEquiv, 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, Representation.Equiv.toLinearEquiv_toLinearMap, 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, AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val, 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, Representation.TensorProduct.assoc_symm_toLinearMap, fixedReduce_eq_one, Submodule.mulMap_comm, mapMatrix_toLinearMap, TensorProduct.gradedMul_def, Finsupp.linearCombination_one_tmul, QuadraticMap.IsometryEquiv.map_radical, 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, Bundle.Trivialization.linearMapAt_def_of_mem, Submodule.coe_prodEquivOfIsCompl, mk_coe, Matrix.toLinearEquiv'_symm_apply, AffineEquiv.toAffineMap_mk, mem_fixedSubmodule_transvection_iff, comp_toLinearMap_eq_iff, Polynomial.comap_taylorEquiv_degreeLT, Units.toLinearMap_mulLeftLinearEquiv, lTensorHomEquivHomLTensor_toLinearMap, LinearMap.intrinsicStar_mul', mem_dilatransvections_iff_rank, fixedSubmodule_eq_top_iff, IsLocalizedModule.iso_symm_comp, TensorProduct.AlgebraTensorModule.rTensor_tensor, Submodule.Quotient.equiv_symm, 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, Pi.intrinsicStar_comul, LinearMap.rTensor_injective_iff_subtype, multilinearMapCongrRight_symm_apply, Bundle.Pretrivialization.linearMapAt_def_of_mem, RootPairing.Equiv.coweightEquiv_one, Submodule.map_eq_top_iff, ofSubmodule'_symm_apply, left_inv, LinearMap.IsSymmetric.toLinearMap_symm, Module.Basis.repr_eq_iff, coe_toContinuousLinearEquiv_symm, ClosedSubmodule.closure_map_eq_mapEquiv_closure, 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, mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one, 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, Representation.LinearizeMonoidal.η_toLinearMap, 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, 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, Algebra.TensorProduct.distribBaseChange_comp_includeLeftSubRight, 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, QuadraticMap.IsometryEquiv.map_posDef_iff, 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', Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg, submoduleMap_apply, Representation.coind'_apply_apply, extend_symm_apply, ModuleCat.hom_inv_rightUnitor, mem_dilatransvections_iff_rank_quotient, 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, Representation.freeLift_toLinearMap, eq_comp_toLinearMap_iff, Submodule.Quotient.equiv_symm_apply, LinearMap.toMatrix_map_left, Coalgebra.coassoc, snd_comp_prodAssoc, TensorProduct.toLinearMap_congr, Representation.Equiv.toLinearMap_mk', comp_symm_cancel_right, Submodule.orderIsoMapComap_symm_apply, LinearMap.toMatrixOrthonormal_apply, Submodule.toLinearMap_prodEquivOfIsCompl_symm, fixedReduce_eq_smul_iff, toModuleIsoₛ_hom, coe_ofIsUnitDet, toLinearMap_eq_coe, comp_coe, Submodule.map_eq_bot_iff, Submodule.reflection_map, Submodule.det_reflection, toModuleIsoₛ_inv, AddMonoidAlgebra.supported_eq_map, 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, 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, RootPairing.polarizationEquiv_toLinearMap, AlgEquiv.toLinearEquiv_toLinearMap, isSymmetric_symm_iff, MonoidAlgebra.supportedEquivFinsupp_apply_support_val, 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, Representation.Equiv.toIntertwiningMap_mk', rTensorHomEquivHomRTensor_toLinearMap, Representation.TensorProduct.toLinearMap_assoc, 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, isIntertwining_symm_isIntertwining, 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, ofSubmodule'_apply, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, transvection.coe_toLinearMap, Rep.indCoindIso_inv_hom_toLinearMap, Ideal.pi_mkQ_rTensor, ClosedSubmodule.mapEquiv_apply, toFGModuleCatIso_hom, ModuleCat.extendScalars_η, TensorProduct.comul_def, MonoidAlgebra.supported_eq_map, det_mul_det_symm, Module.fgSystem.equiv_comp_of, ModuleCat.uliftFunctor_map, LinearMap.surjective_compr₂ₛₗ_of_equiv, toFun_eq_coe, Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap, PointedCone.maxTensorProduct_comm, RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root', mem_stabilizer_fixedSubmodule, rank_map_eq, Module.Relations.Solution.IsPresentation.of_linearEquiv, LinearMap.det_conj, instDiscreteTopologySubtypeMemSubmoduleIntComap, ModuleCat.Hom.hom₂_apply, Representation.LinearizeMonoidal.μ_toLinearMap, TensorProduct.toLinearMap_symm_lid, 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, fixedReduce_mk, MulOpposite.comul_def, Coalgebra.coassoc_symm, 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, LinearIsometryEquiv.toMatrix_mem_unitaryGroup, Algebra.Generators.H1Cotangent.δ_comp_equiv, QuadraticMap.IsometryEquiv.map_negDef_iff, Orientation.map_apply, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm, arrowCongrAddEquiv_apply, Submodule.map_range_rTensor_subtype_lid, LinearMap.mul'_tensor, extend_apply, det_coe_symm, ModuleCat.extendScalars_δ, 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, LinearMap.toMatrix_map_right, Module.Basis.constr_def, finrank_map_eq, toLinearMap_ofTop, AdicCompletion.congr_apply, ModuleCat.extendScalars_ε, 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, Representation.Equiv.toLinearMap_symm, 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, Representation.TensorProduct.toLinearMap_rid, CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap, Derivation.linearEquiv_coe_comp, LieAlgebra.Extension.twoCocycleOf_coe_coe, Submodule.mem_map_equiv, mem_dilatransvections_iff_finrank_quotient, RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection, 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, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, ModuleCat.extendScalars_μ, 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, map_eq_of_mem_fixingSubgroup, Polynomial.taylorLinearEquiv_apply_coe, Representation.TensorProduct.toLinearMap_comm, 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', fixedReduce_mkQ, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, SpecialLinearGroup.toLinearEquiv_to_linearMap, Submodule.comap_unop_mul, LinearMap.IsPositive.toLinearMap_symm, 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, Representation.TensorProduct.toLinearMap_lid, DirectSum.coe_congrLinearEquiv, LinearMap.rTensor_tensor, Representation.LinearizeMonoidal.ε_toLinearMap, Polynomial.map_taylorEquiv_degreeLT, Submodule.Quotient.equiv_apply, 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, Units.mulLeftLinearEquiv_trans_mulLeftLinearEquiv, 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, 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, Bundle.Trivialization.coe_coordChangeL, 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, Units.mulRightLinearEquiv_trans_mulRightLinearEquiv, LinearMap.BilinForm.congr_congr, Equiv.tensorProductAssoc_def, TensorProduct.comm_trans_comm, mapMatrix_trans, comp_coe, trans_refl, AffineEquiv.ofLinearEquiv_trans_ofLinearEquiv, TensorProduct.assoc_tensor'', AffineSubspace.linear_equivMapOfInjective, symm_trans_cancel_right, trans_symm_cancel_left, Bundle.Trivialization.coordChangeL_symm_apply, Module.Basis.mulOpposite_repr_eq, LinearMap.BilinForm.flip_flip, rTensor_trans_apply, transvection.trans_of_left_eq, trans_smul, congrRight₂_trans, TensorProduct.tensorTensorTensorComm_trans_tensorTensorTensorComm, CoalgEquiv.trans_toLinearEquiv, comm_trans_rTensor_trans_comm_eq, 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, Module.Basis.span_neg, 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, Submodule.Quotient.equiv_trans, trans_symm_cancel_right, TensorProduct.rightComm_def, Bundle.Trivialization.coe_coordChangeL', 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	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike ofInvolutive LinearMap LinearMap.instFunLike	—	—
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	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomInvPair.ids
coe_symm_mk' 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom RingHom.id Semiring.toNonAssocSemiring	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring 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 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom toLinearMap	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	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike	—	—
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	3 math math: toSemilinearEquiv_symm_apply, toSemilinearEquiv_apply, symm_toSemilinearEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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	—	RingEquivClass.toRingHomClass instRingEquivClass RingHomInvPair.symm RingHomInvPair.of_ringEquiv
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	2238 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, TensorProduct.AlgebraTensorModule.distribBaseChange_symm_tmul, Finsupp.snd_sumFinsuppLEquivProdFinsupp, LinearEquiv.coe_toEquiv, RootPairing.InvariantForm.apply_reflection_reflection, IsLocalizedModule.iso_symm_apply', Polynomial.degreeLT.addLinearEquiv_symm_apply_inr, Finsupp.fst_sumFinsuppLEquivProdFinsupp, LinearMap.restrictScalars_toMatrix, Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply, LinearMap.apply_symm_toPerfPair_self, LinearMap.SeparatingRight.toMatrix₂', LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, Submodule.rTensorOne_symm_apply, AddMonoidAlgebra.supportedEquivFinsupp_apply_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, Module.bijOn_reflection_of_mapsTo, 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, LinearMap.adjoint_adjoint, IsSemisimpleModule.exists_submodule_linearEquiv_quotient, Matrix.SeparatingRight.toLinearMap₂, LinearEquiv.lTensor_pow, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, Rep.MonoidalClosed.linearHomEquiv_symm_hom, Ideal.tensorCotangentEquiv_tmul, 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, ContinuousAffineMap.fst_decompLinearEquiv, TensorProduct.congr_congr, Bundle.Trivialization.linearEquivAt_symm_apply, 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, Units.mulLeftLinearEquiv_trans_mulLeftLinearEquiv, 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, LinearEquiv.mk_coe', 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, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_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, PowerBasis.repr_pow_isIntegral, LinearMap.exists_linearEquiv_eq_graph, AlternatingMap.constLinearEquivOfIsEmpty_apply, Representation.Equiv.mk_apply, LinearMap.orthogonal_ker, 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, Module.Dual.extendRCLikeₗ_symm_apply, 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.extend_eq, 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, 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, TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_symm_apply_mk_tmul, Matrix.toLin_mul_apply, LinearMap.tensorEqLocusEquiv_apply, toMatrix_distrib_mul_action_toLinearMap, ModuleCat.Iso.homCongr_eq_arrowCongr, AlgEquiv.linearEquivConj_mulLeft, Units.symm_mulLeftLinearEquiv, LinearIsometryEquiv.coe_mk, 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, Algebra.FormallyUnramified.finite_of_free_aux, 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, LinearMap.ker_self_comp_adjoint, Fintype.linearIndependent_iff', AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val, 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.isHermitian_toMatrix_iff, LinearMap.toMatrix_baseChange, RootPairing.toPerfPair_comp_root, TensorProduct.adjoint_map, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, LinearEquiv.conj_comp, LinearIsometryEquiv.lTensor_apply, LinearEquiv.domMulActCongrRight_apply, LinearEquiv.piCurry_apply, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply, LinearMap.ker_adjoint_comp_self, 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, Bundle.Trivialization.localFrame_coeff_eq_coeff, LinearEquiv.map_zero, Module.equiv_directSum_of_isTorsion, dotProductEquiv_apply_apply, DirectSum.lid_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, LinearEquiv.fixedReduce_eq_one, TensorProduct.leftComm_tmul, exteriorPower.alternatingMapLinearEquiv_symm_map, LinearEquiv.symm_apply_eq, TensorProduct.comm_comm, LinearEquiv.coe_isometryOfOrthonormal, 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, LinearMap.IsSymmetric.conj_adjoint, 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, DirectSum.bracket_apply_apply, Pi.counit_eq_adjoint, Unitization.linearEquiv_symm_apply, LinearEquiv.eq_symm_apply, Matrix.toLin'_mul_apply, MultilinearMap.fromDirectSumEquiv_symm_apply, Matrix.toLinearMapₛₗ₂'_single, Matrix.toLin'_hadamard, 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', TensorProduct.quotTensorEquivQuotSMul_mk_one_tmul, 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, Module.FinitePresentation.equiv_quotient, TensorProduct.gradedComm_algebraMap_tmul, IsAdjoinRootMonic.basis_repr, LinearMap.toMatrix_transpose, WeakDual.toStrongDual_inj, LinearMap.toMatrix₂_toLinearMapₛₗ₂, TensorProduct.finsuppLeft_smul', AffineEquiv.congrLeftₗ_symm_apply, Algebra.TensorProduct.basisAux_map_smul, Pi.basis_repr_single, PiTensorProduct.reindex_comp_tprod, LinearIsometryEquiv.coe_toLinearEquiv, Submodule.goursat, 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, RootPairing.mem_range_root_of_mem_range_reflection_of_mem_range_root, 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, ContinuousAffineMap.decompLinearEquiv_symm_contLinear, 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, Algebra.Extension.tensorCotangentSpace_tmul_tmul, 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, LinearMap.isSymmetric_self_comp_adjoint, 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, 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, Units.toLinearMap_mulLeftLinearEquiv, Module.Invertible.rTensorEquiv_apply_apply, Rep.coindVEquiv_symm_apply_coe, LinearEquiv.lTensor_tmul, RootPairing.coreflection_inv, Module.Basis.linearMap_apply, LinearMap.det_toLpLin, 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, NormedSpace.inclusionInDoubleDualWeak_apply_apply, LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo, RootPairing.Equiv.weightMap_weightEquiv_symm, Representation.coinvariantsTprodLeftRegularLEquiv_apply, Matrix.piLinearEquiv_apply, ZMod.dft_comp_unitMul, LinearMap.toMatrix₂_compl₂, LinearEquiv.baseChange_symm_tmul, 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, RootPairing.mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot, 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, WithVal.linearEquiv_apply, NormedSpace.toLinearMap_inclusionInDoubleDualWeak, lp.zeroBasis_repr_apply, Matrix.linfty_opNNNorm_toMatrix, KaehlerDifferential.tensorKaehlerEquivBase_tmul, Module.Basis.coe_constrL, MulOpposite.isometry_opLinearEquiv, LinearEquiv.comp_symm_eq, DirectSum.lid_symm_apply, Submodule.botEquivPUnit_symm_apply, TensorProduct.map_map_assoc_symm, Module.Basis.addSubgroupOfClosure_repr_apply, Algebra.traceForm_toMatrix, KaehlerDifferential.tensorKaehlerEquivBase_symm_apply, Module.Basis.span_repr_eq_single, 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, IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp, 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, 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, Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply, 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.IsSymmetric.adjoint_conj, WithConv.congrLinearEquiv_apply, LinearMap.prodEquiv_symm_apply, PiLp.basisFun_repr, Matrix.toLpLin_pow, KaehlerDifferential.tensorKaehlerEquiv_tmul, Module.AEval'.X_pow_smul_of, Units.toEquiv_mulLeftLinearEquiv, 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, Matrix.isSymmetric_toEuclideanLin_iff, TensorProduct.gradedComm_tmul_of_zero, LinearMap.isNilpotent_toMatrix_iff, Units.mulRightLinearEquiv_mul_apply, TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply, LinearMap.BilinForm.dotProduct_toMatrix_mulVec, LinearMap.det_eq_det_toMatrix_of_finset, LinearMap.toMatrix_reindexRange, IsTensorProduct.assocOfMapSMul_symm_tmul, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, LinearMap.IsReflective.reflective_reflection, Matrix.ofLp_toLpLin, TensorPower.galgebra_toFun_def, Module.range_piEquiv, LinearEquiv.cast_apply, LinearMap.adjoint_comp_self_injective_iff, 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, WithConv.matrixToLin'StarAlgEquiv_apply, MultilinearMap.fromDFinsuppEquiv_single, LinearMap.det_toLin', Submodule.linearEquiv_det_reflection, DirectSum.coe_congr_linearEquiv, Module.FinitePresentation.exists_fin, 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, LinearEquiv.extendOfIsometry_symm_eq, 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, MonoidAlgebra.coeffLinearEquiv_symm_apply, 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, Representation.Equiv.toLinearEquiv_apply, Matrix.SeparatingLeft.toBilin, Matrix.charpoly_toLin, Module.subsingletonEquiv_symm_apply, LinearEquiv.toLinearMap_injective, LinearEquiv.extendScalarsOfIsLocalization_symm_apply, IsTensorProduct.assoc_symm_tmul, 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, LinearEquiv.transvection_mem_dilatransvections, 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, LinearEquiv.mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one, 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, AffineEquiv.arrowCongrₗ_symm_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, 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, Bundle.Trivialization.coe_coordChangeL, 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, StrongDual.extendRCLikeₗ_apply, Module.Basis.singleton_repr, TensorProduct.map_comm, Algebra.Extension.tensorCotangentSpace_tmul, LinearEquiv.coe_toContinuousLinearEquiv_symm', Submodule.le_linearEquiv_of_le_sSup, NormedSpace.inclusionInDoubleDualWeak_apply, Module.AEval.X_pow_smul_of, LinearMap.hasEigenvalue_adjoint_comp_self_sq_singularValues, 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, LinearEquiv.image_closure_of_convex, 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, RootPairing.Base.apply_mem_range_root_of_cartanMatrixEq, LinearEquiv.arrowCongr_apply, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, Algebra.Generators.H1Cotangent.δAux_ofComp, LinearMap.isPositive_toContinuousLinearMap_iff, Matrix.range_toLin', LinearEquiv.apply_smulCommClass, WithVal.linearEquiv_symm_apply, LinearEquiv.finTwoArrow_apply, Submodule.prodEquivOfIsCompl_symm_apply, ZMod.dft_apply, LinearEquiv.skewProd_symm_apply, Representation.linHom.invariantsEquivRepHom_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, PowerBasis.repr_mul_isIntegral, Rep.resCoindHomEquiv_symm_apply, 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, Module.Basis.sum_repr_mul_repr, Matrix.isPositive_toEuclideanLin_iff, AlgEquiv.ofLinearEquiv_apply, 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, AddMonoidAlgebra.coeffLinearEquiv_apply, 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, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, LinearIsometryEquiv.withLpProdCongr_symm_apply, LinearEquiv.conj_symm_conj, Bundle.Pretrivialization.linearEquivAt_symm_apply, LinearMap.toMatrix_algebraMap, LinearEquiv.coe_curry_symm, LinearMap.spectrum_toMatrix, PowerBasis.constr_pow_gen, LinearEquiv.refl_mem_dilatransvections, Submodule.range_lsum_smul, IsBaseChange.equiv_symm_apply, TensorProduct.congr_symm_tmul, LinearMap.SeparatingRight.toMatrix₂, Matrix.isUnit_toLin_iff, Polynomial.degreeLT.addLinearEquiv_apply', LinearEquiv.coe_isometryOfInner, 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, LinearIsometry.adjoint_comp_self', Matrix.toLin'_pow, RootPairing.IsOrthogonal.reflection_apply_right, Module.Basis.mem_span_image, LinearIsometryEquiv.toLinearEquiv_smul, LinearEquiv.symm_smul, Rep.coindVEquiv_apply, Module.Dual.extendRCLikeₗ_apply, 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, DirectSum.decomposeLinearEquiv_apply_coe, 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, 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, Bundle.Trivialization.linearEquivAt_apply, LinearEquiv.lieConj_apply, IsBaseChange.linearMapLeftRightHom_toMatrix, Submodule.quotientEquivOfIsCompl_apply_mk_coe, LinearEquiv.mem_dilatransvections_iff_rank_quotient, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, DFinsupp.lsum_single, LinearEquiv.uniqueProd_symm_apply, Matrix.toLinOfInv_symm_apply, Submodule.smul_top_eq_range_lsum, 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, Representation.Equiv.toLinearEquiv_injective, 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.toMatrix_map_left, LinearMap.BilinForm.mul_toMatrix', QuadraticForm.tensorAssoc_symm_apply, LinearEquiv.extend_symm_eq, 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, LinearEquiv.fixedReduce_eq_smul_iff, 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, StrongDual.extendRCLikeₗ_symm_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', LinearMap.singularValues_fin, LinearMap.sq_singularValues_of_lt, 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, LinearMap.finrank_range_adjoint, 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, LinearMap.sq_singularValues_fin, Matrix.reindexLinearEquiv_mul, Module.Basis.smul_eq_map, finsuppLEquivDirectSum_single, TensorProduct.assocIsometry_apply, Matrix.toLin_conjTranspose, Submodule.quotientEquivOfIsCompl_symm_apply, LinearMap.range_adjoint_comp_self, Module.Relations.Solution.IsPresentation.uniq_symm_var, LinearEquiv.conj_conj_symm, Algebra.TensorProduct.distribBaseChange_includeLeftSubRight_apply, 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, MonoidAlgebra.coeffLinearEquiv_apply, DirectSum.decomposeLinearEquiv_apply, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, 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, WeakDual.isBounded_toWeakDual_preimage_iff_isBounded, 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, 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, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, 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, IsTensorProduct.assoc_tmul, 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, Matrix.isSymmetric_toLin_iff, LinearEquiv.ofLeftInverse_apply, LinearMap.toMatrix'_id, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearMap.polyCharpolyAux_coeff_eval, RingEquiv.toSemilinearEquiv_symm_apply, LinearEquiv.baseChange_inv, RootPairing.Equiv.coweightHom_op, MonoidAlgebra.supportedEquivFinsupp_apply_support_val, 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.symm_mk, LinearEquiv.funUnique_apply, TensorProduct.directSum_symm_lof_tmul, LinearEquiv.sumArrowLequivProdArrow_apply_fst, Rep.coindResAdjunction_homEquiv_symm_apply, LinearEquiv.coe_zero, Matrix.toLinearMapRight'_apply, IsTensorProduct.assocOfMapSMul_tmul, LinearEquiv.continuous_symm, LinearMap.BilinForm.toMatrix_mul, WithAbs.linearEquiv_symm_apply, Finsupp.lcongr_single, LinearEquiv.submoduleMap_symm_apply, LinearMap.GeneralLinearGroup.coe_toLinearEquiv, LinearEquiv.canLiftContinuousLinearEquiv, Matrix.ofLp_toEuclideanLin_apply, AffineEquiv.arrowCongrₗ_apply, Matrix.toLinearMap₂_apply, Finsupp.linearEquivFunOnFinite_apply, Units.symm_mulLeftLinearEquiv_apply, linearEquiv_det_rotation, ZLattice.abs_repr_lt_of_norm_lt, Complex.coe_selfAdjointEquiv, MultilinearMap.freeDFinsuppEquiv_apply, MonoidAlgebra.supportedEquivFinsupp_apply_apply, 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, AddMonoidAlgebra.coeffLinearEquiv_symm_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, Matrix.linfty_opNorm_toMatrix, exteriorPower.zeroEquiv_ιMulti, LinearEquiv.transvection.coe_apply, Matrix.toBilin'_apply', Matrix.toLinearMap₂'_single, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply, Bundle.Trivialization.coordChangeL_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, Rep.indResHomEquiv_apply, CliffordAlgebra.reverseEquiv_symm_apply, WithLp.linearEquiv_apply, LinearEquiv.ofSubmodule'_apply, LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous, 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.dilatransvection.baseChange, 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, RootPairing.coroot_eq_coreflection_of_root_eq, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul, WithConv.symm_matrixToLin'StarAlgEquiv_apply, 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, Rep.resCoindHomEquiv_apply, 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, Matrix.isSymm_iff_intrinsicStar_toLin', ZMod.dft_const_mul, TensorPower.one_mul, Finsupp.domLCongr_apply, RootPairing.isFixedPt_reflection_of_isOrthogonal, LinearMap.linearEquivOfInjective_apply, PiTensorProduct.norm_eval_le_projectiveSeminorm, ContinuousAffineMap.decompLinearEquiv_symm_apply, 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, LinearEquiv.mem_stabilizer_fixedSubmodule, Matrix.toLinearEquivRight'OfInv_apply, hasEigenvalue_toLin'_diagonal_iff, LinearEquiv.map_smul, LinearEquiv.smul_id_of_finrank_eq_one_apply, LinearMap.toMatrix'_toLinearMapₛₗ₂', DirectSum.lequivCongrLeft_symm_lof, 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, RingEquiv.symm_toSemilinearEquiv_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, TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_apply_tmul, QuadraticForm.tensorAssoc_apply, RootPairing.coroot'_reflection, LinearMap.toContPerfPair_apply, Matrix.toEuclideanLin_apply_piLp_toLp, Representation.Equiv.coe_symm, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply, 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, ContinuousLinearEquiv.homothety_inverse, 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, WeakDual.isBounded_toStrongDual_preimage_iff_isBounded, 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, StrongDual.toWeakDual_apply, 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, 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, LinearMap.isSymmetric_adjoint_comp_self, LinearEquiv.nonempty_equiv_iff_rank_eq, LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl, Matrix.kroneckerTMulAlgEquiv_apply, RootPairing.reflection_inv, LieAlgebra.SemiDirectSum.toProdl_coe, Module.End.mem_invtSubmodule_adjoint_iff, ZSpan.map_fundamentalDomain, LinearEquiv.ofIsUnitDet_apply, WithAbs.linearEquiv_apply, LinearMap.nondegenerate_toMatrix₂_iff, LieEquiv.toLinearEquiv_injective, AlgEquiv.linearEquivConj_mulRight, LinearMap.range_self_comp_adjoint, ModuleCat.Iso.conj_eq_conj, MeasureTheory.Measure.addHaar_preimage_linearEquiv, Matrix.toLin_one, Bundle.Pretrivialization.linearEquivAt_apply, Units.mulLeftLinearEquiv_mul_apply, 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, AddEquiv.linearEquiv_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, WithConv.symm_congrLinearEquiv_apply, Submodule.lTensorOne_tmul, LinearEquiv.fixedReduce_mk, instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId, Matrix.Nondegenerate.toBilin', LinearEquiv.isUniformEmbedding, 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, LinearEquiv.reduce_mk, 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₀, LinearEquiv.ext_iff, Function.Exact.linearEquivOfSurjective_symm_apply, Unitization.linearEquiv_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, WeakDual.isBounded_closedBall, 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, ZLattice.covolume.tendsto_card_le_div'', Module.Invertible.linearEquivOfRightInverse_apply, SpecialLinearGroup.coe_toGeneralLinearGroup_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis, LinearEquiv.baseChange_pow, Module.Basis.ofZLatticeComap_repr_apply, LinearIsometryEquiv.toMatrix_mem_unitaryGroup, starLinearEquiv_apply, AlternatingMap.domDomCongrₗ_symm_apply, Rep.indResHomEquiv_symm_apply, Units.symm_mulRightLinearEquiv_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, LinearEquiv.extendOfIsometry_eq, 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, lp.zeroBasis_repr_symm_apply_coe, 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, ContinuousAffineMap.snd_decompLinearEquiv, 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, LinearMap.orthogonal_range, LinearEquiv.pow_apply, LinearEquiv.symmEquiv_symm_apply_symm_apply, LinearMap.BilinForm.Nondegenerate.toMatrix', AlternatingMap.domLCongr_apply, Module.Basis.constr_self, LinearMap.singularValues_of_lt, 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, LinearMap.coe_toContinuousLinearMap_symm, Matrix.range_diagonal, ZMod.completedLFunction_one_sub_even, Representation.leftRegularMapEquiv_symm_single, LinearEquiv.ofIsUnitDet_symm_apply, Matrix.piLinearEquiv_symm_apply, LinearMap.toMatrix_map_right, LinearMap.extendScalarsOfIsLocalizationEquiv_symm_apply, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, Module.reflection_apply, Module.Basis.constr_def, 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, Unitary.toLinearEquiv_mulLeft, Module.Basis.reindexFinsetRange_repr, LinearEquiv.transvection_mem_transvections, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, Submodule.goursat_surjective, 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', DirectSum.decomposeLinearEquiv_symm_lof, AlternatingMap.domDomCongrₗ_apply, KaehlerDifferential.tensorKaehlerEquiv_tmul_D, Module.surjective_piEquiv_apply_iff, LinearMap.transvection.congr, SpecialLinearGroup.coe_mk, ZSpan.repr_floor_apply, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, 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, LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm, Submodule.mem_biSup_iff_exists_dfinsupp, LinearEquiv.one_eq_refl, Module.Basis.tensorProduct_repr_tmul_apply, Module.Basis.coe_ofEquivFun, Representation.freeLiftLEquiv_symm_apply, 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, DirectSum.lequivCongrLeft_lof, Module.Basis.sum_equivFun, WithLp.coe_symm_linearEquiv, IsSemisimpleModule.exists_linearEquiv_dfinsupp, 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, LinearMap.self_comp_adjoint_injective_iff, 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, Submodule.exists_equiv_eq_graph, 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, Representation.leftRegularMapEquiv_apply, SpecialLinearGroup.baseChange_apply_coe, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, LinearEquiv.instSemilinearEquivClass, LinearEquiv.ofInjective_symm_apply, Representation.Equiv.dualTensorHom_invFun, 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, LinearMap.IsSymmetric.toMatrix_eigenvectorBasis, Module.Basis.repr_eq_iff', LinearMap.toLinearMap_toPerfPair, LinearEquiv.mem_dilatransvections_iff_finrank_quotient, RootPairing.coroot_reflectionPerm, ZLattice.covolume.tendsto_card_div_pow'', TensorProduct.gradedComm_of_tmul_of, PowerBasis.constr_pow_aeval, Submodule.map_equivMapOfInjective_symm_apply, Representation.Equiv.coe_invFun, LinearEquiv.image_closure_of_convex', 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, LinearEquiv.mem_stabilizer_submodule_of_le_fixedSubmodule, Representation.Equiv.conj_apply_self, Module.Basis.det_map, LieModule.shiftedGenWeightSpace.shift_symm_apply, LinearMap.posSemidef_toMatrix_iff, Matrix.coe_ofLinearEquiv, ZMod.LFunction_dft, Module.Basis.norm_repr_le_norm, LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero', LinearEquiv.smul_refl, Representation.freeLiftLEquiv_apply, 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, LinearMap.toMatrix₂'_apply, Submodule.FG.rTensor.directLimit_apply', Submodule.image_smul_top_eq_range_lsum, 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.coe_directSumRight, 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, Bundle.Trivialization.localFrame_coeff_apply_of_mem_baseSet, Submodule.sndEquiv_symm_apply_coe, Matrix.toLinearMapₛₗ₂_toMatrix₂, Submodule.comapSubtypeEquivOfLe_symm_apply, Module.Basis.coord_apply, LinearMap.toMatrix'_mulVec, TensorProduct.AlgebraTensorModule.distribBaseChange_tmul, 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, Units.mulLeftLinearEquiv_apply, hasEigenvector_toLin_diagonal, LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero, Units.mulRightLinearEquiv_apply, 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, 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, LinearEquiv.reduce_mkQ, AlgEquiv.eq_linearEquivConjAlgEquiv, 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, LinearEquiv.fixedReduce_mkQ, 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, AffineEquiv.congrLeftₗ_apply, 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, 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, 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, AddEquiv.linearEquiv_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, Representation.leftRegularMapEquiv_symm_apply_toFun, 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, isSemisimpleModule_iff_exists_linearEquiv_dfinsupp, 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	6 math math: AlgEquivClass.toLinearEquivClass, Representation.Equiv.instLinearEquivClass, 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