Equiv

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

Statistics

Metric	Count
Definitions apply, symm_apply, arrowCongrEquiv, automorphismGroup, equivLike, equivOfInverse, equivOfInverse', equivOfRightInverse, finTwoArrow, funUnique, instSMulUnitsId, neg, ofEq, ofSubmodule', ofSubmodules, ofUnit, piCongrLeft, piCongrRight, piFinTwo, piUnique, prodAssoc, prodComm, prodCongr, prodProdProdComm, prodUnique, refl, skewProd, smulLeft, submoduleMap, sumPiEquivProdPi, toContinuousLinearMap, toHomeomorph, toLinearEquiv, toUnit, trans, ulift, uniqueProd, unitsEquiv, unitsEquivAut, ContinuousLinearEquivClass, IsInvertible, finCons, iInfKerProjEquiv, inverse, ContinuousSemilinearEquivClass, consEquivL, opContinuousLinearEquiv, «term_≃L[_]_», «term_≃SL[_]_»	49
Theorems apply_symm_apply, arrowCongrEquiv_apply, arrowCongrEquiv_symm_apply, bijective, coe_apply, coe_coe, coe_comp_coe_symm, coe_funUnique, coe_funUnique_symm, coe_inj, coe_injective, coe_mk, coe_neg, coe_prodAssoc, coe_prodCongr, coe_prodProdProdComm, coe_prodUnique, coe_refl, coe_refl', coe_symm_comp_coe, coe_symm_toHomeomorph, coe_symm_toLinearEquiv, coe_toHomeomorph, coe_toLinearEquiv, coe_uniqueProd, comp_coe, comp_continuousOn_iff, comp_continuous_iff, continuous, continuousAt, continuousOn, continuousSemilinearEquivClass, continuousWithinAt, continuous_invFun, continuous_toFun, eq_comp_toContinuousLinearMap_symm, eq_symm_apply, eq_toContinuousLinearMap_symm_comp, equivOfInverse'_apply, equivOfInverse_apply, equivOfRightInverse_symm_apply, ext, ext_iff, ext₁, finTwoArrow_apply, finTwoArrow_symm_apply, fst_equivOfRightInverse, image_closure, image_eq_preimage_symm, image_symm_eq_preimage, image_symm_image, injective, isClosed_image, isOpenMap, isUniformEmbedding, map_add, map_eq_zero_iff, map_neg, map_nhds_eq, map_smul, map_smulₛₗ, map_sub, map_zero, neg_apply, ofSubmodule'_apply, ofSubmodule'_symm_apply, ofSubmodule'_toContinuousLinearMap, ofSubmodules_apply, ofSubmodules_symm_apply, piCongrRight_apply, piCongrRight_symm_apply, piFinTwo_apply, piFinTwo_symm_apply, piUnique_apply, piUnique_symm_apply, preimage_closure, preimage_symm_preimage, prodAssoc_apply, prodAssoc_symm_apply, prodAssoc_toLinearEquiv, prodComm_apply, prodComm_symm, prodComm_toLinearEquiv, prodCongr_apply, prodCongr_symm, prodProdProdComm_apply, prodProdProdComm_symm, prodProdProdComm_toLinearEquiv, prodUnique_apply, prodUnique_symm_apply, refl_apply, refl_symm, self_comp_symm, self_trans_symm, skewProd_apply, skewProd_symm_apply, smulLeft_apply_apply, smulLeft_apply_toLinearEquiv, smul_apply, smul_trans, snd_equivOfRightInverse, submoduleMap_apply, submoduleMap_symm_apply, surjective, symm_apply_apply, symm_apply_eq, symm_bijective, symm_comp_self, symm_equivOfInverse, symm_equivOfInverse', symm_image_image, symm_map_nhds_eq, symm_neg, symm_preimage_preimage, symm_smul, symm_smul_apply, symm_symm, symm_symm_apply, symm_trans_apply, symm_trans_self, toHomeomorph_symm, toLinearEquiv_injective, toLinearEquiv_smul, toLinearEquiv_symm, trans_apply, trans_smul, trans_toLinearEquiv, uniqueProd_apply, uniqueProd_symm_apply, unitsEquivAut_apply, unitsEquivAut_apply_symm, unitsEquivAut_symm_apply, unitsEquiv_apply, bijective, comp, injective, inverse, inverse_apply_eq, inverse_apply_self, inverse_comp_apply_of_left, inverse_comp_apply_of_right, inverse_comp_of_left, inverse_comp_of_right, inverse_comp_self, inverse_inverse, of_inverse, of_isInvertible_inverse, self_apply_inverse, self_comp_inverse, surjective, coprod_comp_prodComm, inverse_comp_equiv, inverse_eq, inverse_eq_ringInverse, inverse_equiv, inverse_equiv_comp, inverse_id, inverse_of_not_isInvertible, inverse_zero, isInvertible_comp_equiv, isInvertible_equiv, isInvertible_equiv_comp, isInvertible_inverse_iff, isInvertible_zero_iff, ringInverse_eq_inverse, ringInverse_equiv, continuousSemilinearMapClass, instHomeomorphClass, inv_continuous, map_continuous, toSemilinearEquivClass, consEquivL_apply, consEquivL_symm_apply, isUniformEmbedding, opContinuousLinearEquiv_apply, opContinuousLinearEquiv_symm_apply, exists_submodule_equiv_prod	177
Total	226

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
arrowCongrEquiv 📖	CompOp	2 math math: arrowCongrEquiv_symm_apply, arrowCongrEquiv_apply
automorphismGroup 📖	CompOp	3 math math: unitsEquiv_apply, smulLeft_apply_apply, smulLeft_apply_toLinearEquiv
equivLike 📖	CompOp	330 math math: preimage_symm_preimage, antilipschitz, PiLp.continuousLinearEquiv_symm_apply, StarModule.decomposeProdAdjointL_symm_apply, symm_preimage_preimage, LinearEquiv.norm_extend_le, equivOfInverse'_apply, unitsEquiv_apply, coe_toHomeomorph, differentiable, image_closure, Manifold.IsImmersionAtOfComplement.target_subset_preimage_target, toCompactConvergenceCLM_symm_apply, Manifold.IsImmersionAt.map_target_subset_target, contDiff_comp_iff, coe_prodAssoc, Matrix.l2_opNorm_mulVec, map_sub, snd_equivOfRightInverse, coe_toSpanNonzeroSingleton_symm, map_tsum, LinearEquiv.extend_eq, comp_right_differentiableWithinAt_iff, hasSum', toCompactConvergenceCLM_apply, coe_toDiffeomorph_symm, WithLp.prodContinuousLinearEquiv_symm_apply, apply_symm_apply, hasTemperateGrowth, isOpenMap, comp_hasFDerivAt_iff, ext_iff, map_smul, StarModule.decomposeProdAdjointL_apply, SchwartzMap.compCLMOfContinuousLinearEquiv_apply, contDiffAt_comp_iff, isBigO_comp, IsCoercive.unique_continuousLinearEquivOfBilin, PiLp.coe_continuousLinearEquiv, NumberField.mixedEmbedding.negAt_apply_snd, symm_trans_apply, InnerProductSpace.harmonicOnNhd_comp_CLE_iff, RCLike.conjCLE_apply, Fin.consEquivL_apply, Euclidean.closedBall_eq_image, NumberField.mixedEmbedding.negAt_preimage, ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_apply, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, coeFn_ofBijective, Manifold.IsImmersionAtOfComplement.map_target_subset_target, SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv, Trivialization.continuousLinearEquivAt_apply, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, unitsEquivAut_apply, comp_differentiableOn_iff, SeparatingDual.exists_continuousLinearEquiv_apply_eq, starL_apply, piUnique_symm_apply, uniqueProd_symm_apply, VectorField.pullbackWithin_eq_of_fderivWithin_eq, finTwoArrow_symm_apply, isAddHaarMeasure_map, compContinuousAlternatingMap_coe, coe_toContinuousAffineEquiv, arrowCongr_apply, ContinuousLinearMap.coe_equivRange, isBigO_sub, hasMFDerivAt, VectorBundleCore.trivializationAt_coordChange_eq, piUnique_apply, Complex.equivRealProdCLM_symm_apply, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, hasMFDerivWithinAt, uniqueDiffOn_image, comp_fderiv, LinearIsometryEquiv.coe_toContinuousLinearEquiv, integral_comp_comm, comp_right_fderiv, Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm, ContinuousAlgEquiv.toContinuousLinearEquiv_apply, Manifold.IsImmersionAt.writtenInCharts, ProbabilityTheory.isGaussian_map_equiv_iff, starL'_apply, bijective, differentiableAt, Matrix.l2_opNNNorm_mulVec, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, FiberwiseLinear.trans_openPartialHomeomorph_apply, integrable_comp_iff, symm_smul_apply, ContinuousLinearMap.equivRange_symm_apply, injective, PointwiseConvergenceCLM.equivWeakDual_apply, Module.Basis.equivFunL_symm_apply_repr, contDiffPointwiseHolderAt, ContinuousLinearMap.coe_flipMultilinearEquiv, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, MulOpposite.opContinuousLinearEquiv_symm_apply, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, prodComm_apply, NumberField.mixedEmbedding.volume_preserving_negAt, PointwiseConvergenceCLM.equivWeakDual_symm_apply, NumberField.mixedEmbedding.negAt_apply_isComplex, dimH_image, WithLp.prodContinuousLinearEquiv_symm_apply_ofLp, finTwoArrow_apply, mdifferentiableOn, FourierTransform.fourierCLE_apply, SchwartzMap.fourierTransformCLE_apply, LinearEquiv.coe_toContinuousLinearEquiv', NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, Module.Basis.equivFunL_apply, Trivialization.continuousLinearEquivAt_apply', LinearEquiv.coe_toContinuousLinearEquiv_symm', InnerProductSpace.harmonicAt_comp_CLE_iff, coe_toLinearEquiv, comp_right_hasFDerivAt_iff, lipschitz, LinearIsometryEquiv.coe_coe, refl_apply, CStarMatrix.ofMatrix_eq_ofMatrixL, hasSum, comp_hasFDerivWithinAt_iff', equivOfInverse_apply, starL_symm_apply, toSpanNonzeroSingleton_symm_apply, analyticOn, ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero_apply, hasFDerivWithinAt, comp_right_hasFDerivWithinAt_iff, comp_continuousOn_iff, ofSubmodule'_apply, strictConvex_image, coe_prodProdProdComm, LinearEquiv.extend_symm_apply, ContinuousLinearMap.coprodEquivL_apply_apply, skewProd_apply, isBigO_sub_rev, isUniformEmbedding, VectorBundleCore.localTriv_coordChange_eq, coe_neg, comp_hasFDerivWithinAt_iff, smulLeft_apply_apply, LinearEquiv.extend_symm_eq, coord_toSpanNonzeroSingleton, prodUnique_symm_apply, coe_mk, SchwartzMap.fourierTransformCLE_symm_apply, starL'_symm_apply, unitsEquivAut_symm_apply, coe_symm_toHomeomorph, map_neg, uniqueProd_apply, toSpanNonzeroSingleton_coord, comp_right_hasFDerivWithinAt_iff', neg_apply, MeasureTheory.Measure.addHaar_image_continuousLinearEquiv, unitsEquivAut_apply_symm, comp_right_differentiableOn_iff, symm_comp_self, iteratedFDeriv_comp_left, coe_apply, image_eq_preimage_symm, surjective, ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv_symm, contDiffWithinAt_comp_iff, self_comp_symm, Trivialization.apply_eq_prod_continuousLinearEquivAt, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, image_symm_eq_preimage, NumberField.mixedEmbedding.volume_negAt_plusPart, prodAssoc_apply, map_smulₛₗ, Trivialization.coordChangeL_symm_apply, Euclidean.closedBall_eq_preimage, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, Trivialization.mk_coordChangeL, ProbabilityTheory.HasGaussianLaw.map_equiv, fderiv, mdifferentiableWithinAt, mdifferentiable, comp_differentiableAt_iff, comp_hasFDerivAt_iff', map_eq_zero_iff, continuousAlternatingMapCongrLeft_apply, map_add, symm_symm_apply, comp_right_differentiableAt_iff, Complex.conjCLE_apply, differentiableOn, hasStrictFDerivAt, mfderiv_eq, Trivialization.coe_continuousLinearEquivAt_eq, comp_contDiffWithinAt_iff, Euclidean.ball_eq_preimage, Trivialization.continuousLinearEquivAt_symm_apply, LinearIsometryEquiv.coe_symm_toContinuousLinearEquiv, LinearEquiv.norm_extend_symm_le, Trivialization.coordChangeL_apply, continuousAlternatingMapCongrRight_apply, continuous, symm_image_image, LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous, MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv, continuousSemilinearEquivClass, ProbabilityTheory.HasGaussianLaw.map_equiv_fun, comp_contDiffOn_iff, Manifold.IsImmersionAt.target_subset_preimage_target, eq_symm_apply, arrowCongrSL_apply, submoduleMap_symm_apply, ModelWithCorners.transContinuousLinearEquiv_range, skewProd_symm_apply, continuousMultilinearMapCongrLeft_apply, Shrink.continuousLinearEquiv_symm_apply, comp_differentiable_iff, Trivialization.symm_continuousLinearEquivAt_eq, contDiffOn_comp_iff, IsCoercive.continuousLinearEquivOfBilin_apply, fderivWithin, isBigO_comp_rev, tsum_eq_iff, coe_toDiffeomorph, continuousAt, ContinuousLinearMap.prodL_apply, Complex.equivRealProdCLM_symm_apply_re, prodUnique_apply, trans_apply, Manifold.IsImmersionAtOfComplement.writtenInCharts, comp_continuous_iff, FourierTransform.fourierCLE_symm_apply, NumberField.mixedEmbedding.normAtPlace_negAt, Shrink.continuousLinearEquiv_apply, Trivialization.coe_coordChangeL, map_zero, smul_apply, submoduleMap_apply, ofBijective_symm_apply_apply, uniqueDiffOn_preimage_iff, Submodule.ClosedComplemented.exists_submodule_equiv_prod, isClosed_image, NumberField.mixedEmbedding.negAt_apply_norm_isReal, hasFDerivAt, summable, analyticOnNhd, ofSubmodule'_symm_apply, prodProdProdComm_apply, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, VectorField.pullback_eq_of_fderiv_eq, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, PiLp.coe_symm_continuousLinearEquiv, dimH_preimage, continuousAlternatingMapCongr_apply, ProbabilityTheory.isGaussian_map_equiv, Complex.equivRealProdCLM_symm_apply_im, continuousMultilinearMapCongrRight_apply, analyticWithinAt, ModelWithCorners.coe_transContinuousLinearEquiv, LinearEquiv.extend_apply, map_nhds_eq, MulOpposite.opContinuousLinearEquiv_apply, Trivialization.apply_symm_apply_eq_coordChangeL, uniqueDiffOn_image_iff, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, symm_apply_apply, ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv, WithCStarModule.equivL_symm_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, arrowCongrSL_symm_apply, Module.Basis.map_addHaar, toSpanNonzeroSingleton_apply_coe, Trivialization.prod_apply', comp_fderivWithin, coe_coe, strictConvex_preimage, differentiableWithinAt, preimage_closure, analyticAt, ModelWithCorners.coe_transContinuousLinearEquiv_symm, comp_contDiff_iff, symm_apply_eq, LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm, PiLp.continuousLinearEquiv_apply, comp_contDiffAt_iff, InnerProductSpace.laplacian_CLE_comp_left, comp_right_hasFDerivAt_iff', prodCongr_apply, image_symm_image, FiberwiseLinear.trans_PartialHomeomorph_apply, WithCStarModule.equivL_apply, iteratedFDerivWithin_comp_left, continuousOn, prodAssoc_symm_apply, fst_equivOfRightInverse, NumberField.mixedEmbedding.norm_negAt, ContinuousLinearMap.toSpanSingletonCLE_apply_apply, ContinuousLinearMap.toSpanSingletonCLE_symm_apply, symm_map_nhds_eq, contDiffPointwiseHolderAt_left_comp, comp_differentiableWithinAt_iff, InnerProductSpace.laplacianWithin_CLE_comp_left, equivOfRightInverse_symm_apply, Fin.consEquivL_symm_apply, mdifferentiableAt, piCongrRight_symm_apply, conjContinuousAlgEquiv_apply_apply, continuousWithinAt, ContinuousLinearMap.coprodEquivL_symm_apply, coe_funUnique_symm, piCongrRight_apply, Submodule.coe_prodEquivOfClosedCompl, NumberField.mixedEmbedding.disjoint_negAt_plusPart, piFinTwo_symm_apply, Trivialization.coordChangeL_apply', coe_refl', comp_right_differentiable_iff, Complex.equivRealProdCLM_apply, coe_symm_toLinearEquiv, coe_funUnique, symm_conjContinuousAlgEquiv_apply_apply, Submodule.coe_prodEquivOfClosedCompl_symm, ofSubmodules_apply, piFinTwo_apply, comp_hasStrictFDerivAt_iff, mfderivWithin_eq, contDiff, ModelWithCorners.extChartAt_transContinuousLinearEquiv_target, ofBijective_apply_symm_apply, WithLp.prodContinuousLinearEquiv_apply, ofSubmodules_symm_apply
equivOfInverse 📖	CompOp	2 math math: equivOfInverse_apply, symm_equivOfInverse
equivOfInverse' 📖	CompOp	2 math math: equivOfInverse'_apply, symm_equivOfInverse'
equivOfRightInverse 📖	CompOp	3 math math: snd_equivOfRightInverse, fst_equivOfRightInverse, equivOfRightInverse_symm_apply
finTwoArrow 📖	CompOp	2 math math: finTwoArrow_symm_apply, finTwoArrow_apply
funUnique 📖	CompOp	2 math math: coe_funUnique_symm, coe_funUnique
instSMulUnitsId 📖	CompOp	8 math math: symm_smul_apply, symm_smul, trans_smul, toLinearEquiv_smul, conjContinuousAlgEquiv_ext_iff, smul_trans, smul_apply, LinearIsometryEquiv.toContinuousLinearEquiv_smul
neg 📖	CompOp	4 math math: symm_neg, coe_neg, neg_apply, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero
ofEq 📖	CompOp	—
ofSubmodule' 📖	CompOp	3 math math: ofSubmodule'_apply, ofSubmodule'_symm_apply, ofSubmodule'_toContinuousLinearMap
ofSubmodules 📖	CompOp	2 math math: ofSubmodules_apply, ofSubmodules_symm_apply
ofUnit 📖	CompOp	—
piCongrLeft 📖	CompOp	—
piCongrRight 📖	CompOp	2 math math: piCongrRight_symm_apply, piCongrRight_apply
piFinTwo 📖	CompOp	2 math math: piFinTwo_symm_apply, piFinTwo_apply
piUnique 📖	CompOp	2 math math: piUnique_symm_apply, piUnique_apply
prodAssoc 📖	CompOp	4 math math: coe_prodAssoc, prodAssoc_apply, prodAssoc_toLinearEquiv, prodAssoc_symm_apply
prodComm 📖	CompOp	4 math math: ContinuousLinearMap.coprod_comp_prodComm, prodComm_apply, prodComm_symm, prodComm_toLinearEquiv
prodCongr 📖	CompOp	6 math math: prodCongr_symm, coe_prodCongr, Continuous.prod_map_equivL, Trivialization.continuousLinearEquivAt_prod, prodCongr_apply, ContinuousOn.prod_map_equivL
prodProdProdComm 📖	CompOp	4 math math: prodProdProdComm_symm, coe_prodProdProdComm, prodProdProdComm_toLinearEquiv, prodProdProdComm_apply
prodUnique 📖	CompOp	3 math math: prodUnique_symm_apply, prodUnique_apply, coe_prodUnique
refl 📖	CompOp	14 math math: conjContinuousAlgEquiv_refl, Bundle.Trivial.continuousLinearEquivAt_trivialization, ContinuousAlgEquiv.refl_toContinuousLinearEquiv, refl_apply, coe_refl, refl_symm, fderiv_continuousLinearEquiv_comp, LinearIsometryEquiv.toContinuousLinearEquiv_refl, symm_trans_self, Bundle.Trivial.trivialization.coordChangeL, fderivWithin_continuousLinearEquiv_comp, self_trans_symm, fderiv_continuousLinearEquiv_comp', coe_refl'
skewProd 📖	CompOp	2 math math: skewProd_apply, skewProd_symm_apply
smulLeft 📖	CompOp	2 math math: smulLeft_apply_apply, smulLeft_apply_toLinearEquiv
submoduleMap 📖	CompOp	2 math math: submoduleMap_symm_apply, submoduleMap_apply
sumPiEquivProdPi 📖	CompOp	—
toContinuousLinearMap 📖	CompOp	196 math math: antilipschitz, ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, isConformalMap_conj, LinearIsometryEquiv.hasStrictFDerivAt, LinearIsometryEquiv.comp_fderiv, ContinuousLinearMap.HasRightInverse.comp_continuousLinearEquivalence, ContinuousLinearMap.HasRightInverse.continuousLinearEquivalence_comp, hasRightInverse, RCLike.conjCLE_norm, ContinuousAlgEquiv.toContinuousLinearMap_toContinuousLinearEquiv_eq, LinearIsometryEquiv.comp_fderivWithin, subsingleton_or_norm_symm_pos, LinearIsometryEquiv.fderivWithin, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, coe_comp_coe_symm, mdifferentiableOn_symm_coordChangeL, ContinuousLinearMap.coprod_comp_prodComm, IsConformalMap.is_complex_or_conj_linear, LinearIsometryEquiv.conjStarAlgEquiv_apply, ContinuousLinearMap.isInvertible_comp_equiv, comp_hasFDerivAt_iff, Unitary.coe_linearIsometryEquiv_apply, ContinuousLinearMap.coe_toContinuousLinearEquivOfDetNeZero, HasStrictFDerivAt.star, ContinuousLinearMap.HasLeftInverse.comp_continuousLinearEquivalence, HasFDerivAt.star, Unitary.linearIsometryEquiv_coe_apply, ContinuousLinearMap.coe_equivProdOfSurjectiveOfIsCompl, LinearIsometryEquiv.adjoint_eq_symm, Submodule.IsOrtho.map_iff, fderivWithin_star, Submodule.coe_orthogonalDecomposition_symm, MeasureTheory.charFunDual_pi', continuousAlternatingMapCongrLeftEquiv_apply, conjContinuousAlgEquiv_apply, hasLeftInverse, ContinuousLinearMap.inverse_equiv, LinearIsometryEquiv.fderiv, one_le_norm_mul_norm_symm, HasFDerivWithinAt.star, hasMFDerivAt, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff', unitary.linearIsometryEquiv_coe_symm_apply, hasMFDerivWithinAt, contDiffAt_map_inverse, comp_fderiv, toContinuousAffineEquiv_toContinuousAffineMap, ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp, comp_right_fderiv, ContinuousLinearMap.ringInverse_equiv, Unitary.coe_symm_linearIsometryEquiv_apply, PiLp.hasFDerivAt_toLp, ContMDiffOn.coordChangeL, iteratedFDerivWithin_comp_right, LinearEquiv.coe_toContinuousLinearEquiv_symm, MDifferentiableOn.coordChangeL, coe_symm_comp_coe, contMDiffAt_coordChangeL, eq_toContinuousLinearMap_symm_comp, coe_inj, MDifferentiableWithinAt.coordChangeL, Diffeomorph.mfderivToContinuousLinearEquiv_coe, Submodule.coe_orthogonalDecomposition, comp_coe, coe_prodCongr, nhds, ContinuousLinearMap.isInvertible_equiv, VectorBundle.continuousOn_coordChange', ContinuousLinearMap.coe_linearMap_equivRange, LinearIsometryEquiv.completeSpace_map, Unitary.linearIsometryEquiv_coe_symm_apply, comp_right_hasFDerivAt_iff, lipschitz, eq_comp_toContinuousLinearMap_symm, comp_hasFDerivWithinAt_iff', ProbabilityTheory.indepFun_iff_charFunDual_prod', comp_right_fderivWithin, coe_refl, hasFDerivWithinAt, comp_right_hasFDerivWithinAt_iff, contMDiffOn_symm_coordChangeL, ofSubmodule'_apply, ImplicitFunctionData.hasStrictFDerivAt, Submodule.sndL_comp_coe_orthogonalDecomposition, norm_symm_pos, subsingleton_or_nnnorm_symm_pos, comp_hasFDerivWithinAt_iff, LinearIsometryEquiv.coe_coe'', coe_injective, HasFDerivAtFilter.star, Complex.conjCLE_nnorm, IsLocalDiffeomorph.mfderivToContinuousLinearEquiv_coe, comp_right_hasFDerivWithinAt_iff', MeasureTheory.Measure.addHaar_image_continuousLinearEquiv, iteratedFDeriv_comp_left, FormalMultilinearSeries.leftInv_coeff_one, coe_apply, LinearIsometryEquiv.hasFDerivAt, HasDerivAt.hasFDerivAt_equiv, det_coe_symm, rightInverse_hasRightInverse, isConformalMap_complex_linear_conj, LinearIsometryEquiv.submoduleMap_symm_apply_coe, Submodule.IsOrtho.comap_iff, fderiv, LinearEquiv.coe_toContinuousLinearEquiv, Complex.conjCLE_enorm, comp_hasFDerivAt_iff', fderiv_continuousLinearEquiv_comp, continuousAlternatingMapCongrLeft_apply, hasStrictFDerivAt, mfderiv_eq, mdifferentiableOn_coordChangeL, continuousAlternatingMapCongrRight_apply, ContinuousLinearMap.inverse_comp_equiv, ContMDiffVectorBundle.contMDiffOn_coordChangeL, ContinuousLinearMap.inCoordinates_eq, LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv, arrowCongrEquiv_symm_apply, leftInverse_hasLeftInverse, MDifferentiableAt.coordChangeL, arrowCongrSL_apply, submoduleMap_symm_apply, MeasureTheory.charFunDual_prod', ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl, EuclideanGeometry.hasFDerivAt_inversion, PiLp.hasFDerivAt_ofLp, continuousMultilinearMapCongrLeft_apply, fderivWithin, isOpen, arrowCongrEquiv_apply, MeasureTheory.charFunDual_eq_pi_iff', ContinuousLinearMap.inverse_equiv_comp, LinearIsometryEquiv.comp_hasFDerivAt_iff', FormalMultilinearSeries.radius_compContinuousLinearMap_le, LinearIsometryEquiv.comp_hasFDerivAt_iff, ContMDiffWithinAt.coordChangeL, ContinuousLinearMap.inverse_eq_ringInverse, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv, submoduleMap_apply, fderiv_star, hasFDerivAt, fderivWithin_continuousLinearEquiv_comp, LinearIsometryEquiv.hasFDerivWithinAt, Submodule.fstL_comp_coe_orthogonalDecomposition, continuousAlternatingMapCongrRightEquiv_apply, ofSubmodule'_symm_apply, Complex.conjCLE_norm, mdifferentiableAt_coordChangeL, ContinuousLinearMap.HasLeftInverse.continuousLinearEquivalence_comp, LinearIsometryEquiv.star_eq_symm, continuousAlternatingMapCongr_apply, RCLike.toContinuousLinearMap_complexLinearIsometryEquiv, continuousMultilinearMapCongrRight_apply, FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2, nnnorm_symm_pos, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff, contMDiffOn_coordChangeL, arrowCongrSL_symm_apply, Module.Basis.opNNNorm_le, comp_fderivWithin, coe_coe, PiLp.hasStrictFDerivAt_ofLp, Module.Basis.opNorm_le, comp_right_hasFDerivAt_iff', HasStrictDerivAt.hasStrictFDerivAt_equiv, exists_continuousLinearEquiv_fderiv_symm_eq, FormalMultilinearSeries.rightInv_coeff, coe_ofBijective, ContinuousLinearMap.isInvertible_equiv_comp, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe, iteratedFDerivWithin_comp_left, arrowCongrSL_toLinearEquiv_apply, HasFDerivAt.star_star, exists_continuousLinearEquiv_fderivWithin_symm_eq, FormalMultilinearSeries.rightInv_coeff_one, fderiv_continuousLinearEquiv_comp', isConformalMap_iff_is_complex_or_conj_linear, MeasureTheory.charFunDual_eq_prod_iff', arrowCongrSL_toLinearEquiv_symm_apply, continuousOn_coordChange, LinearIsometryEquiv.comp_fderiv', mem_contMDiffFiberwiseLinear_iff, ofSubmodule'_toContinuousLinearMap, LinearIsometryEquiv.comp_hasStrictFDerivAt_iff, ContMDiff.coordChangeL, norm_pos, comp_hasStrictFDerivAt_iff, mfderivWithin_eq, LinearIsometryEquiv.submoduleMap_apply_coe, PiLp.hasStrictFDerivAt_toLp, unitary.linearIsometryEquiv_coe_apply, Trivialization.coordChangeL_prod
toHomeomorph 📖	CompOp	3 math math: coe_toHomeomorph, coe_symm_toHomeomorph, toHomeomorph_symm
toLinearEquiv 📖	CompOp	35 math math: Pi.comul_eq_adjoint, toLinearEquiv_symm, ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_toLinearEquiv, instIsZLatticeComap, LinearEquiv.toLinearEquiv_toContinuousLinearEquiv_symm, Pi.counit_eq_adjoint, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, RCLike.conjCLE_coe, trans_toLinearEquiv, ContinuousLinearMap.equivRange_symm_toLinearEquiv, coe_toLinearEquiv, LinearEquiv.toLinearEquiv_toContinuousLinearEquiv, toLinearEquiv_smul, continuous_invFun, coe_uniqueProd, prodAssoc_toLinearEquiv, Trivialization.coe_coordChangeL', prodProdProdComm_toLinearEquiv, LinearEquiv.canLiftContinuousLinearEquiv, ContinuousAlgEquiv.toContinuousLinearEquiv_toLinearEquiv_eq, toLinearEquiv_injective, instDiscreteTopologySubtypeMemSubmoduleIntComap, ZLattice.covolume_comap, Module.Basis.ofZLatticeBasis_comap, Equiv.toLinearEquiv_continuousLinearEquiv, coe_prodUnique, Module.Basis.map_addHaar, continuous_toFun, smulLeft_apply_toLinearEquiv, arrowCongrSL_toLinearEquiv_apply, arrowCongrSL_toLinearEquiv_symm_apply, prodComm_toLinearEquiv, ofSubmodule'_toContinuousLinearMap, coe_symm_toLinearEquiv, Complex.conjCLE_coe
toUnit 📖	CompOp	—
trans 📖	CompOp	12 math math: symm_trans_apply, ContinuousAlgEquiv.trans_toContinuousLinearEquiv, Trivialization.comp_continuousLinearEquivAt_eq_coord_change, conjContinuousAlgEquiv_trans, trans_toLinearEquiv, comp_coe, trans_smul, trans_apply, smul_trans, LinearIsometryEquiv.toContinuousLinearEquiv_trans, symm_trans_self, self_trans_symm
ulift 📖	CompOp	—
uniqueProd 📖	CompOp	3 math math: uniqueProd_symm_apply, uniqueProd_apply, coe_uniqueProd
unitsEquiv 📖	CompOp	1 math math: unitsEquiv_apply
unitsEquivAut 📖	CompOp	5 math math: unitsEquivAut_apply, unitsEquivAut_symm_apply, unitsEquivAut_apply_symm, HasDerivAt.hasFDerivAt_equiv, HasStrictDerivAt.hasStrictFDerivAt_equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	LinearEquiv.right_inv
arrowCongrEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousLinearMap EquivLike.toFunLike Equiv.instEquivLike arrowCongrEquiv ContinuousLinearMap.comp toContinuousLinearMap symm	—	—
arrowCongrEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv ContinuousLinearMap EquivLike.toFunLike Equiv.instEquivLike Equiv.symm arrowCongrEquiv ContinuousLinearMap.comp toContinuousLinearMap symm	—	—
bijective 📖	mathematical	—	Function.Bijective DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Equiv.bijective
coe_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike toContinuousLinearMap ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	—
coe_coe 📖	mathematical	—	DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike toContinuousLinearMap ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	—
coe_comp_coe_symm 📖	mathematical	—	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ toContinuousLinearMap symm ContinuousLinearMap.id	—	ContinuousLinearMap.ext RingHomInvPair.triples₂ apply_symm_apply
coe_funUnique 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike equivLike funUnique Function.eval Unique.instInhabited	—	RingHomInvPair.ids
coe_funUnique_symm 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike equivLike symm funUnique	—	RingHomInvPair.ids
coe_inj 📖	mathematical	—	toContinuousLinearMap	—	coe_injective
coe_injective 📖	mathematical	—	ContinuousLinearEquiv ContinuousLinearMap toContinuousLinearMap	—	ext ContinuousLinearMap.ext_iff
coe_mk 📖	mathematical	Continuous AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom LinearEquiv.toLinearMap LinearEquiv.invFun	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike LinearEquiv LinearEquiv.instEquivLike	—	—
coe_neg 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike equivLike neg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	RingHomInvPair.ids
coe_prodAssoc 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike prodAssoc Equiv Equiv.instEquivLike Equiv.prodAssoc	—	RingHomInvPair.ids
coe_prodCongr 📖	mathematical	—	toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule prodCongr ContinuousLinearMap.prodMap	—	RingHomInvPair.ids
coe_prodProdProdComm 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike prodProdProdComm Equiv Equiv.instEquivLike Equiv.prodProdProdComm	—	RingHomInvPair.ids
coe_prodUnique 📖	mathematical	—	LinearEquiv.toEquiv Prod.instAddCommMonoid Prod.instModule RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids toLinearEquiv instTopologicalSpaceProd prodUnique Equiv.prodUnique	—	RingHomInvPair.ids
coe_refl 📖	mathematical	—	toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids refl ContinuousLinearMap.id	—	RingHomInvPair.ids
coe_refl' 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike refl	—	RingHomInvPair.ids
coe_symm_comp_coe 📖	mathematical	—	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ toContinuousLinearMap symm ContinuousLinearMap.id	—	ContinuousLinearMap.ext RingHomInvPair.triples₂ symm_apply_apply
coe_symm_toHomeomorph 📖	mathematical	—	DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm toHomeomorph ContinuousLinearEquiv equivLike symm	—	—
coe_symm_toLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toLinearEquiv ContinuousLinearEquiv equivLike symm	—	—
coe_toHomeomorph 📖	mathematical	—	DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike toHomeomorph ContinuousLinearEquiv equivLike	—	—
coe_toLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike LinearEquiv.instEquivLike toLinearEquiv ContinuousLinearEquiv equivLike	—	—
coe_uniqueProd 📖	mathematical	—	LinearEquiv.toEquiv Prod.instAddCommMonoid Prod.instModule RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids toLinearEquiv instTopologicalSpaceProd uniqueProd Equiv.uniqueProd	—	RingHomInvPair.ids
comp_coe 📖	mathematical	—	ContinuousLinearMap.comp toContinuousLinearMap trans	—	—
comp_continuousOn_iff 📖	mathematical	—	ContinuousOn DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Homeomorph.comp_continuousOn_iff
comp_continuous_iff 📖	mathematical	—	Continuous DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Homeomorph.comp_continuous_iff
continuous 📖	mathematical	—	Continuous DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	continuous_toFun
continuousAt 📖	mathematical	—	ContinuousAt DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Continuous.continuousAt continuous
continuousOn 📖	mathematical	—	ContinuousOn DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Continuous.continuousOn continuous
continuousSemilinearEquivClass 📖	mathematical	—	ContinuousSemilinearEquivClass ContinuousLinearEquiv equivLike	—	AddHom.map_add' LinearMap.map_smul' continuous_toFun continuous_invFun
continuousWithinAt 📖	mathematical	—	ContinuousWithinAt DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Continuous.continuousWithinAt continuous
continuous_invFun 📖	mathematical	—	Continuous LinearEquiv.invFun toLinearEquiv	—	—
continuous_toFun 📖	mathematical	—	Continuous AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom LinearEquiv.toLinearMap toLinearEquiv	—	—
eq_comp_toContinuousLinearMap_symm 📖	mathematical	—	ContinuousLinearMap.comp toContinuousLinearMap symm	—	ContinuousLinearMap.ext symm_apply_apply apply_symm_apply
eq_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	LinearEquiv.eq_symm_apply
eq_toContinuousLinearMap_symm_comp 📖	mathematical	—	ContinuousLinearMap.comp toContinuousLinearMap symm	—	ContinuousLinearMap.ext apply_symm_apply symm_apply_apply
equivOfInverse'_apply 📖	mathematical	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ ContinuousLinearMap.id	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike equivOfInverse' ContinuousLinearMap ContinuousLinearMap.funLike	—	RingHomInvPair.triples₂
equivOfInverse_apply 📖	mathematical	DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike	ContinuousLinearEquiv EquivLike.toFunLike equivLike equivOfInverse	—	—
equivOfRightInverse_symm_apply 📖	mathematical	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	ContinuousLinearEquiv RingHomInvPair.ids Submodule SetLike.instMembership Submodule.setLike LinearMap.ker ContinuousLinearMap.toLinearMap instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike equivLike symm equivOfRightInverse AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomInvPair.ids
ext 📖	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	—	toLinearEquiv_injective LinearEquiv.ext
ext_iff 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	ext
ext₁ 📖	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule EquivLike.toFunLike equivLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	RingHomInvPair.ids ext smul_eq_mul map_smul mul_one
finTwoArrow_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace Pi.addCommMonoid instTopologicalSpaceProd Prod.instAddCommMonoid Pi.Function.module Prod.instModule EquivLike.toFunLike equivLike finTwoArrow	—	RingHomInvPair.ids
finTwoArrow_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Pi.topologicalSpace Pi.addCommMonoid Prod.instModule Pi.Function.module EquivLike.toFunLike equivLike symm finTwoArrow Matrix.vecCons Matrix.vecEmpty	—	RingHomInvPair.ids
fst_equivOfRightInverse 📖	mathematical	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	Submodule SetLike.instMembership Submodule.setLike LinearMap.ker ContinuousLinearMap.toLinearMap ContinuousLinearEquiv RingHomInvPair.ids instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike equivLike equivOfRightInverse	—	RingHomInvPair.ids
image_closure 📖	mathematical	—	Set.image DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike closure	—	Homeomorph.image_closure
image_eq_preimage_symm 📖	mathematical	—	Set.image DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike Set.preimage symm	—	Equiv.image_eq_preimage_symm
image_symm_eq_preimage 📖	mathematical	—	Set.image DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm Set.preimage	—	image_eq_preimage_symm symm_symm
image_symm_image 📖	mathematical	—	Set.image DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	symm_image_image
injective 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Equiv.injective
isClosed_image 📖	mathematical	—	IsClosed Set.image DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Homeomorph.isClosed_image
isOpenMap 📖	mathematical	—	IsOpenMap DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Homeomorph.isOpenMap
isUniformEmbedding 📖	mathematical	—	IsUniformEmbedding DFunLike.coe ContinuousLinearEquiv UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid EquivLike.toFunLike equivLike	—	Equiv.isUniformEmbedding ContinuousLinearMap.uniformContinuous
map_add 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	ContinuousLinearMap.map_add
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LinearEquiv.map_eq_zero_iff
map_neg 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Ring.toSemiring AddCommGroup.toAddCommMonoid EquivLike.toFunLike equivLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	ContinuousLinearMap.map_neg
map_nhds_eq 📖	mathematical	—	Filter.map DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike nhds	—	Homeomorph.map_nhds_eq
map_smul 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids ContinuousLinearMap.map_smul
map_smulₛₗ 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike 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	—	ContinuousLinearMap.map_smulₛₗ
map_sub 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Ring.toSemiring AddCommGroup.toAddCommMonoid EquivLike.toFunLike equivLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	ContinuousLinearMap.map_sub
map_zero 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	ContinuousLinearMap.map_zero
neg_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike equivLike neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
ofSubmodule'_apply 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousLinearEquiv Submodule.comap ContinuousLinearMap.toLinearMap toContinuousLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module EquivLike.toFunLike equivLike ofSubmodule'	—	—
ofSubmodule'_symm_apply 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike Submodule.comap ContinuousLinearMap.toLinearMap toContinuousLinearMap DFunLike.coe ContinuousLinearEquiv instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module EquivLike.toFunLike equivLike symm ofSubmodule'	—	—
ofSubmodule'_toContinuousLinearMap 📖	mathematical	—	toContinuousLinearMap Submodule SetLike.instMembership Submodule.setLike Submodule.comap ContinuousLinearMap.toLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ofSubmodule' ContinuousLinearMap.codRestrict LinearEquiv.toLinearMap toLinearEquiv ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Submodule.subtypeL DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike	—	—
ofSubmodules_apply 📖	mathematical	Submodule.map RingHomSurjective.invPair ContinuousLinearMap.toLinearMap toContinuousLinearMap	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousLinearEquiv instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module EquivLike.toFunLike equivLike ofSubmodules	—	RingHomSurjective.invPair
ofSubmodules_symm_apply 📖	mathematical	Submodule.map RingHomSurjective.invPair ContinuousLinearMap.toLinearMap toContinuousLinearMap	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousLinearEquiv instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module EquivLike.toFunLike equivLike symm ofSubmodules	—	RingHomSurjective.invPair
piCongrRight_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace Pi.addCommMonoid Pi.module EquivLike.toFunLike equivLike piCongrRight	—	RingHomInvPair.ids
piCongrRight_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace Pi.addCommMonoid Pi.module EquivLike.toFunLike equivLike symm piCongrRight	—	RingHomInvPair.ids
piFinTwo_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace Pi.addCommMonoid instTopologicalSpaceProd Prod.instAddCommMonoid Pi.module Prod.instModule EquivLike.toFunLike equivLike piFinTwo	—	RingHomInvPair.ids
piFinTwo_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Pi.topologicalSpace Pi.addCommMonoid Prod.instModule Pi.module EquivLike.toFunLike equivLike symm piFinTwo Fin.cons finZeroElim	—	RingHomInvPair.ids
piUnique_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace Pi.addCommMonoid Unique.instInhabited Pi.module EquivLike.toFunLike equivLike piUnique	—	RingHomInvPair.ids
piUnique_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Unique.instInhabited Pi.topologicalSpace Pi.addCommMonoid Pi.module EquivLike.toFunLike equivLike symm piUnique uniqueElim	—	RingHomInvPair.ids
preimage_closure 📖	mathematical	—	Set.preimage DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike closure	—	Homeomorph.preimage_closure
preimage_symm_preimage 📖	mathematical	—	Set.preimage DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	symm_preimage_preimage
prodAssoc_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike prodAssoc	—	RingHomInvPair.ids
prodAssoc_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike symm prodAssoc	—	RingHomInvPair.ids
prodAssoc_toLinearEquiv 📖	mathematical	—	toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule prodAssoc LinearEquiv.prodAssoc	—	RingHomInvPair.ids
prodComm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike prodComm	—	RingHomInvPair.ids
prodComm_symm 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule prodComm	—	RingHomInvPair.ids
prodComm_toLinearEquiv 📖	mathematical	—	toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule prodComm LinearEquiv.prodComm	—	RingHomInvPair.ids
prodCongr_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike prodCongr	—	RingHomInvPair.ids
prodCongr_symm 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule prodCongr	—	RingHomInvPair.ids
prodProdProdComm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike prodProdProdComm	—	RingHomInvPair.ids
prodProdProdComm_symm 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule prodProdProdComm	—	RingHomInvPair.ids
prodProdProdComm_toLinearEquiv 📖	mathematical	—	toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule prodProdProdComm LinearEquiv.prodProdProdComm	—	RingHomInvPair.ids
prodUnique_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike prodUnique	—	RingHomInvPair.ids
prodUnique_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike symm prodUnique Unique.instInhabited	—	RingHomInvPair.ids
refl_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike refl	—	RingHomInvPair.ids
refl_symm 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids refl	—	RingHomInvPair.ids
self_comp_symm 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	apply_symm_apply
self_trans_symm 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomInvPair.triples₂ symm refl	—	ext RingHomInvPair.ids RingHomInvPair.triples₂ symm_apply_apply
skewProd_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike skewProd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ContinuousLinearMap ContinuousLinearMap.funLike	—	RingHomInvPair.ids
skewProd_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike symm skewProd SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ContinuousLinearMap ContinuousLinearMap.funLike	—	RingHomInvPair.ids
smulLeft_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup MonoidHom.instFunLike smulLeft SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	RingHomInvPair.ids
smulLeft_apply_toLinearEquiv 📖	mathematical	—	toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFunLike.coe MonoidHom ContinuousLinearEquiv MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup MonoidHom.instFunLike smulLeft DistribMulAction.toLinearEquiv	—	RingHomInvPair.ids
smul_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike 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 RingHomInvPair.ids RingHomCompTriple.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearEquiv instSMulUnitsId	—	RingHomInvPair.ids ext RingHomCompTriple.ids LinearMapClass.map_smul_of_tower ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousSemilinearEquivClass.continuousSemilinearMapClass continuousSemilinearEquivClass LinearMap.IsScalarTower.compatibleSMul
snd_equivOfRightInverse 📖	mathematical	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	Submodule SetLike.instMembership Submodule.setLike LinearMap.ker ContinuousLinearMap.toLinearMap ContinuousLinearEquiv RingHomInvPair.ids instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike equivLike equivOfRightInverse SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	RingHomInvPair.ids
submoduleMap_apply 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike Submodule.map RingHomSurjective.invPair ContinuousLinearMap.toLinearMap toContinuousLinearMap DFunLike.coe ContinuousLinearEquiv instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module EquivLike.toFunLike equivLike submoduleMap	—	RingHomSurjective.invPair
submoduleMap_symm_apply 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe ContinuousLinearEquiv Submodule.map RingHomSurjective.invPair ContinuousLinearMap.toLinearMap toContinuousLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module EquivLike.toFunLike equivLike symm submoduleMap	—	RingHomSurjective.invPair
surjective 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	Equiv.surjective
symm_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	LinearEquiv.left_inv
symm_apply_eq 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	LinearEquiv.symm_apply_eq
symm_bijective 📖	mathematical	—	Function.Bijective ContinuousLinearEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_comp_self 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	symm_apply_apply
symm_equivOfInverse 📖	mathematical	DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike	symm equivOfInverse	—	—
symm_equivOfInverse' 📖	mathematical	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ ContinuousLinearMap.id	symm equivOfInverse'	—	RingHomInvPair.triples₂
symm_image_image 📖	mathematical	—	Set.image DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	Equiv.symm_image_image
symm_map_nhds_eq 📖	mathematical	—	Filter.map DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm nhds	—	Homeomorph.symm_map_nhds_eq
symm_neg 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid neg	—	RingHomInvPair.ids
symm_preimage_preimage 📖	mathematical	—	Set.preimage DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	Equiv.symm_preimage_preimage
symm_smul 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearEquiv instSMulUnitsId Units.instInv	—	RingHomInvPair.ids
symm_smul_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike 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_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm	—	—
symm_trans_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm trans	—	—
symm_trans_self 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomInvPair.triples₂ symm refl	—	ext RingHomInvPair.ids RingHomInvPair.triples₂ apply_symm_apply
toHomeomorph_symm 📖	mathematical	—	toHomeomorph symm Homeomorph.symm	—	—
toLinearEquiv_injective 📖	mathematical	—	ContinuousLinearEquiv LinearEquiv toLinearEquiv	—	—
toLinearEquiv_smul 📖	mathematical	—	toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearEquiv instSMulUnitsId LinearEquiv LinearEquiv.instSMulUnitsId	—	RingHomInvPair.ids
toLinearEquiv_symm 📖	mathematical	—	toLinearEquiv symm LinearEquiv.symm	—	—
trans_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike trans	—	—
trans_smul 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearEquiv instSMulUnitsId	—	RingHomInvPair.ids ext RingHomCompTriple.ids
trans_toLinearEquiv 📖	mathematical	—	toLinearEquiv trans LinearEquiv.trans	—	LinearEquiv.ext
uniqueProd_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike uniqueProd	—	RingHomInvPair.ids
uniqueProd_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule EquivLike.toFunLike equivLike symm uniqueProd Unique.instInhabited	—	RingHomInvPair.ids
unitsEquivAut_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule EquivLike.toFunLike equivLike Equiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Equiv.instEquivLike unitsEquivAut Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Units.val	—	RingHomInvPair.ids
unitsEquivAut_apply_symm 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule EquivLike.toFunLike equivLike symm Equiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Equiv.instEquivLike unitsEquivAut Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Units.val Units.instInv	—	RingHomInvPair.ids
unitsEquivAut_symm_apply 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe Equiv ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Units EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitsEquivAut equivLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
unitsEquiv_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike MulEquiv Units ContinuousLinearMap MonoidWithZero.toMonoid ContinuousLinearMap.monoidWithZero Units.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup MulEquiv.instEquivLike unitsEquiv ContinuousLinearMap.funLike Units.val	—	RingHomInvPair.ids

ContinuousLinearEquiv.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—
symm_apply 📖	CompOp	—

ContinuousLinearMap

Definitions

Name	Category	Theorems
IsInvertible 📖	MathDef	9 math math: ImplicitFunctionData.isInvertible_fderiv_prodFun, isInvertible_comp_equiv, isInvertible_zero_iff, isInvertible_equiv, IsInvertible.of_inverse, isInvertible_mfderiv_extChartAt, isInvertible_inverse_iff, isInvertible_mfderivWithin_extChartAt_symm, isInvertible_equiv_comp
finCons 📖	CompOp	8 math math: HasStrictFDerivAt.finCons, hasFDerivWithinAt_finCons', hasFDerivAt_finCons', HasFDerivAt.finCons, HasFDerivWithinAt.finCons, hasStrictFDerivAt_finCons', hasFDerivAtFilter_finCons', HasFDerivAtFilter.finCons
iInfKerProjEquiv 📖	CompOp	—
inverse 📖	CompOp	30 math math: IsInvertible.inverse_comp_of_right, IsInvertible.inverse_comp_of_left, inverse_equiv, contDiffAt_map_inverse, ringInverse_equiv, VectorField.mpullback_apply, IsInvertible.inverse_inverse, inverse_eq, IsInvertible.inverse, inverse_zero, IsInvertible.contDiffAt_map_inverse, ringInverse_eq_inverse, inverse_comp_equiv, IsInvertible.inverse_comp_self, IsInvertible.inverse_apply_self, VectorField.pullbackWithin_eq, inverse_of_not_isInvertible, IsInvertible.inverse_comp_apply_of_right, inverse_equiv_comp, VectorField.mpullbackWithin_apply, inverse_eq_ringInverse, inverse_mfderiv_mul_left, isInvertible_inverse_iff, IsInvertible.self_comp_inverse, VectorField.mlieBracketWithin_apply, IsInvertible.self_apply_inverse, IsInvertible.inverse_comp_apply_of_left, inverse_id, inverse_mfderiv_add_left, IsInvertible.inverse_apply_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprod_comp_prodComm 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule RingHomCompTriple.ids coprod ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.prodComm	—	prod_ext RingHomCompTriple.ids RingHomInvPair.ids ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass zero_add coprod_comp_inl add_zero coprod_comp_inr
inverse_comp_equiv 📖	mathematical	—	inverse comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	—	RingHomInvPair.ids RingHomCompTriple.ids inverse_equiv comp.congr_simp inverse_of_not_isInvertible comp_zero
inverse_eq 📖	mathematical	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids id	inverse	—	RingHomCompTriple.ids RingHomInvPair.ids inverse_equiv
inverse_eq_ringInverse 📖	mathematical	—	inverse comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Ring.inverse ContinuousLinearMap monoidWithZero ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	—	RingHomInvPair.ids RingHomCompTriple.ids ext inverse_equiv comp.congr_simp ringInverse_equiv ContinuousLinearEquiv.apply_symm_apply Mathlib.Tactic.Contrapose.contrapose₄ inverse_of_not_isInvertible Ring.inverse_non_unit zero_comp
inverse_equiv 📖	mathematical	—	inverse ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearEquiv.symm	—	RingHomInvPair.ids Classical.choose_eq
inverse_equiv_comp 📖	mathematical	—	inverse comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	—	RingHomInvPair.ids RingHomCompTriple.ids inverse_equiv comp.congr_simp inverse_of_not_isInvertible zero_comp
inverse_id 📖	mathematical	—	inverse id	—	ringInverse_eq_inverse Ring.inverse_one
inverse_of_not_isInvertible 📖	mathematical	IsInvertible	inverse ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring zero	—	RingHomInvPair.ids
inverse_zero 📖	mathematical	—	inverse ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring zero	—	isInvertible_zero_iff ext inverse_of_not_isInvertible
isInvertible_comp_equiv 📖	mathematical	—	IsInvertible comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids RingHomCompTriple.ids ext ContinuousLinearEquiv.apply_symm_apply
isInvertible_equiv 📖	mathematical	—	IsInvertible ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids	—	RingHomInvPair.ids
isInvertible_equiv_comp 📖	mathematical	—	IsInvertible comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids RingHomCompTriple.ids ext ContinuousLinearEquiv.symm_apply_apply
isInvertible_inverse_iff 📖	mathematical	—	IsInvertible inverse	—	IsInvertible.of_isInvertible_inverse IsInvertible.inverse
isInvertible_zero_iff 📖	mathematical	—	IsInvertible ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring zero	—	RingHomInvPair.ids ContinuousLinearEquiv.injective Equiv.subsingleton continuous_of_discreteTopology Subsingleton.discreteTopology ext
ringInverse_eq_inverse 📖	mathematical	—	Ring.inverse ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring monoidWithZero inverse	—	ext RingHomCompTriple.ids RingHomInvPair.ids inverse_eq_ringInverse comp.congr_simp id_comp comp_id
ringInverse_equiv 📖	mathematical	—	Ring.inverse ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring monoidWithZero ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids inverse	—	RingHomInvPair.ids Ring.inverse_invertible invOf_units inverse_equiv

ContinuousLinearMap.IsInvertible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective 📖	mathematical	ContinuousLinearMap.IsInvertible	Function.Bijective DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	RingHomInvPair.ids
comp 📖	mathematical	ContinuousLinearMap.IsInvertible	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomInvPair.ids RingHomCompTriple.ids
injective 📖	mathematical	ContinuousLinearMap.IsInvertible	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	Function.Bijective.injective bijective
inverse 📖	mathematical	ContinuousLinearMap.IsInvertible	ContinuousLinearMap.inverse	—	RingHomInvPair.ids ContinuousLinearMap.inverse_equiv
inverse_apply_eq 📖	mathematical	ContinuousLinearMap.IsInvertible	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike ContinuousLinearMap.inverse	—	RingHomInvPair.ids ContinuousLinearMap.inverse_equiv ContinuousLinearEquiv.symm_apply_eq
inverse_apply_self 📖	mathematical	ContinuousLinearMap.IsInvertible	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike ContinuousLinearMap.inverse	—	RingHomInvPair.ids ContinuousLinearMap.inverse_equiv ContinuousLinearEquiv.symm_apply_apply
inverse_comp_apply_of_left 📖	mathematical	ContinuousLinearMap.IsInvertible	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike ContinuousLinearMap.inverse ContinuousLinearMap.comp RingHomCompTriple.ids	—	RingHomCompTriple.ids inverse_comp_of_left
inverse_comp_apply_of_right 📖	mathematical	ContinuousLinearMap.IsInvertible	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike ContinuousLinearMap.inverse ContinuousLinearMap.comp RingHomCompTriple.ids	—	RingHomCompTriple.ids inverse_comp_of_right
inverse_comp_of_left 📖	mathematical	ContinuousLinearMap.IsInvertible	ContinuousLinearMap.inverse ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomInvPair.ids RingHomCompTriple.ids ContinuousLinearMap.inverse_equiv_comp ContinuousLinearMap.comp.congr_simp ContinuousLinearMap.inverse_equiv
inverse_comp_of_right 📖	mathematical	ContinuousLinearMap.IsInvertible	ContinuousLinearMap.inverse ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomInvPair.ids RingHomCompTriple.ids ContinuousLinearMap.inverse_comp_equiv ContinuousLinearMap.comp.congr_simp ContinuousLinearMap.inverse_equiv
inverse_comp_self 📖	mathematical	ContinuousLinearMap.IsInvertible	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ContinuousLinearMap.inverse ContinuousLinearMap.id	—	RingHomInvPair.ids RingHomCompTriple.ids ContinuousLinearMap.comp.congr_simp ContinuousLinearMap.inverse_equiv ContinuousLinearEquiv.coe_symm_comp_coe
inverse_inverse 📖	mathematical	ContinuousLinearMap.IsInvertible	ContinuousLinearMap.inverse	—	RingHomInvPair.ids ContinuousLinearMap.inverse_equiv
of_inverse 📖	mathematical	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ContinuousLinearMap.id	ContinuousLinearMap.IsInvertible	—	RingHomCompTriple.ids RingHomInvPair.ids
of_isInvertible_inverse 📖	—	ContinuousLinearMap.IsInvertible ContinuousLinearMap.inverse	—	—	RingHomInvPair.ids Unique.instSubsingleton
self_apply_inverse 📖	mathematical	ContinuousLinearMap.IsInvertible	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike ContinuousLinearMap.inverse	—	RingHomInvPair.ids ContinuousLinearMap.inverse_equiv ContinuousLinearEquiv.apply_symm_apply
self_comp_inverse 📖	mathematical	ContinuousLinearMap.IsInvertible	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ContinuousLinearMap.inverse ContinuousLinearMap.id	—	RingHomInvPair.ids RingHomCompTriple.ids ContinuousLinearMap.comp.congr_simp ContinuousLinearMap.inverse_equiv ContinuousLinearEquiv.coe_comp_coe_symm
surjective 📖	mathematical	ContinuousLinearMap.IsInvertible	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	Function.Bijective.surjective bijective

ContinuousSemilinearEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSemilinearMapClass 📖	mathematical	—	ContinuousSemilinearMapClass EquivLike.toFunLike	—	AddEquivClass.map_add SemilinearEquivClass.toAddEquivClass toSemilinearEquivClass SemilinearEquivClass.map_smulₛₗ map_continuous
instHomeomorphClass 📖	mathematical	—	HomeomorphClass	—	map_continuous inv_continuous
inv_continuous 📖	mathematical	—	Continuous EquivLike.inv	—	—
map_continuous 📖	mathematical	—	Continuous DFunLike.coe EquivLike.toFunLike	—	—
toSemilinearEquivClass 📖	mathematical	—	SemilinearEquivClass	—	—

Fin

Definitions

Name	Category	Theorems
consEquivL 📖	CompOp	2 math math: consEquivL_apply, consEquivL_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
consEquivL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace Prod.instAddCommMonoid Pi.addCommMonoid Prod.instModule Pi.module EquivLike.toFunLike ContinuousLinearEquiv.equivLike consEquivL cons	—	RingHomInvPair.ids
consEquivL_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace Pi.addCommMonoid instTopologicalSpaceProd Prod.instAddCommMonoid Pi.module Prod.instModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm consEquivL tail	—	RingHomInvPair.ids

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUniformEmbedding 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe LinearEquiv AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike symm	IsUniformEmbedding	—	ContinuousLinearEquiv.isUniformEmbedding

MulOpposite

Definitions

Name	Category	Theorems
opContinuousLinearEquiv 📖	CompOp	3 math math: opContinuousLinearEquiv_symm_apply, opContinuousLinearEquiv_apply, toContinuousLinearEquiv_opLinearIsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opContinuousLinearEquiv_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOpposite instTopologicalSpaceMulOpposite instAddCommMonoid instModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike opContinuousLinearEquiv op	—	RingHomInvPair.ids
opContinuousLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOpposite instTopologicalSpaceMulOpposite instAddCommMonoid instModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm opContinuousLinearEquiv unop	—	RingHomInvPair.ids

Submodule.ClosedComplemented

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_submodule_equiv_prod 📖	mathematical	Submodule.ClosedComplemented	DFunLike.coe ContinuousLinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Submodule SetLike.instMembership Submodule.setLike instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike ContinuousLinearEquiv.equivLike Submodule.zero ContinuousLinearEquiv.symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomInvPair.ids sub_self ContinuousLinearMap.apply_val_ker sub_zero

(root)

Definitions

Name	Category	Theorems
ContinuousLinearEquivClass 📖	MathDef	—
ContinuousSemilinearEquivClass 📖	CompData	1 math math: ContinuousLinearEquiv.continuousSemilinearEquivClass
«term_≃L[_]_» 📖	CompOp	—
«term_≃SL[_]_» 📖	CompOp	—

---

← Back to Index