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, restrictScalars, skewProd, smulLeft, submoduleMap, sumPiEquivProdPi, toContinuousAddEquiv, toContinuousLinearMap, toHomeomorph, toLinearEquiv, toUnit, trans, ulift, uniqueProd, unitsEquiv, unitsEquivAut, ContinuousLinearEquivClass, IsInvertible, finCons, iInfKerProjEquiv, inverse, ContinuousSemilinearEquivClass, consEquivL, opContinuousLinearEquiv, «term_≃L[_]_», «term_≃SL[_]_»	51
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, restrictScalars_apply, restrictScalars_symm_apply, restrictScalars_toLinearEquiv, 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, toContinuousAddEquiv_coe, 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	181
Total	232

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	351 math math: preimage_symm_preimage, antilipschitz, Bundle.Trivialization.symm_continuousLinearEquivAt_eq, PiLp.continuousLinearEquiv_symm_apply, StarModule.decomposeProdAdjointL_symm_apply, symm_preimage_preimage, LinearEquiv.norm_extend_le, equivOfInverse'_apply, unitsEquiv_apply, coe_toHomeomorph, differentiable, restrictScalars_symm_apply, 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, Bundle.Trivialization.coordChangeL_apply, Bundle.Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm, coe_toSpanNonzeroSingleton_symm, map_tsum, LinearEquiv.extend_eq, comp_right_differentiableWithinAt_iff, hasSum', toCompactConvergenceCLM_apply, coe_toDiffeomorph_symm, VectorField.mlieBracket_smul_left, WithLp.prodContinuousLinearEquiv_symm_apply, restrictScalars_apply, apply_symm_apply, hasTemperateGrowth, isOpenMap, scalarSMulCLE_symm_apply, 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, Bundle.Trivialization.coe_continuousLinearEquivAt_eq, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, HasMFDerivAt.smul, unitsEquivAut_apply, comp_differentiableOn_iff, SeparatingDual.exists_continuousLinearEquiv_apply_eq, starL_apply, fromTangentSpace_mfderiv_smul_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, Bundle.Trivialization.continuousLinearEquivAt_apply', uniqueDiffOn_image, comp_fderiv, toContinuousAddEquiv_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv, integral_comp_comm, comp_right_fderiv, ContinuousAlgEquiv.toContinuousLinearEquiv_apply, Manifold.IsImmersionAt.writtenInCharts, ProbabilityTheory.isGaussian_map_equiv_iff, iteratedFDerivWithin_comp_right, starL'_apply, bijective, Bundle.Trivialization.prod_apply', differentiableAt, Matrix.l2_opNNNorm_mulVec, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, FiberwiseLinear.trans_openPartialHomeomorph_apply, integrable_comp_iff, symm_smul_apply, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, ContinuousLinearMap.equivRange_symm_apply, ClosedSubmodule.mem_mapEquiv_iff', Bundle.Trivialization.apply_symm_apply_eq_coordChangeL, 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, fromTangentSpace_mfderiv_smul_apply', mdifferentiableOn, FourierTransform.fourierCLE_apply, VectorBundle.continuousLinearEquivAt_apply, SchwartzMap.fourierTransformCLE_apply, LinearEquiv.coe_toContinuousLinearEquiv', Bundle.Trivialization.coe_coordChangeL, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, Module.Basis.equivFunL_apply, LinearEquiv.coe_toContinuousLinearEquiv_symm', InnerProductSpace.harmonicAt_comp_CLE_iff, coe_toLinearEquiv, comp_right_hasFDerivAt_iff, lipschitz, LinearIsometryEquiv.coe_coe, VectorField.mlieBracketWithin_smul_left, refl_apply, VectorBundle.continuousLinearEquivAt_symm_apply, CStarMatrix.ofMatrix_eq_ofMatrixL, hasSum, comp_hasFDerivWithinAt_iff', equivOfInverse_apply, starL_symm_apply, comp_right_fderivWithin, toSpanNonzeroSingleton_symm_apply, analyticOn, ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero_apply, hasFDerivWithinAt, comp_right_hasFDerivWithinAt_iff, comp_continuousOn_iff, VectorField.mlieBracketWithin_smul_right, ofSubmodule'_apply, strictConvex_image, coe_prodProdProdComm, LinearEquiv.extend_symm_apply, ContinuousLinearMap.coprodEquivL_apply_apply, scalarSMulCLE_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, Bundle.Trivialization.continuousLinearEquivAt_apply, coe_apply, image_eq_preimage_symm, surjective, ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv_symm, contDiffWithinAt_comp_iff, self_comp_symm, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, Bundle.Trivialization.apply_eq_prod_continuousLinearEquivAt, image_symm_eq_preimage, NumberField.mixedEmbedding.volume_negAt_plusPart, Bundle.Trivialization.continuousLinearEquivAt_symm_apply, prodAssoc_apply, map_smulₛₗ, Euclidean.closedBall_eq_preimage, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, 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, comp_contDiffWithinAt_iff, Euclidean.ball_eq_preimage, LinearIsometryEquiv.coe_symm_toContinuousLinearEquiv, LinearEquiv.norm_extend_symm_le, continuousAlternatingMapCongrRight_apply, continuous, Bundle.Trivialization.coordChangeL_symm_apply, 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, contDiffOn_comp_iff, IsCoercive.continuousLinearEquivOfBilin_apply, fderivWithin, isBigO_comp_rev, ContinuousAlgEquiv.coeCLE_apply, 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, ClosedSubmodule.mem_mapEquiv_iff, Shrink.continuousLinearEquiv_apply, 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, Bundle.Trivialization.mk_coordChangeL, ofSubmodule'_symm_apply, prodProdProdComm_apply, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, Bundle.Trivialization.coordChangeL_apply', VectorField.pullback_eq_of_fderiv_eq, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, PiLp.coe_symm_continuousLinearEquiv, dimH_preimage, continuousAlternatingMapCongr_apply, mfderiv_smul, ProbabilityTheory.isGaussian_map_equiv, Complex.equivRealProdCLM_symm_apply_im, continuousMultilinearMapCongrRight_apply, analyticWithinAt, ModelWithCorners.coe_transContinuousLinearEquiv, LinearEquiv.extend_apply, map_nhds_eq, MulOpposite.opContinuousLinearEquiv_apply, 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, comp_fderivWithin, coe_coe, strictConvex_preimage, differentiableWithinAt, ContinuousAlgEquiv.coe_coeCLE, 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, 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, coe_refl', comp_right_differentiable_iff, Complex.equivRealProdCLM_apply, coe_symm_toLinearEquiv, coe_funUnique, symm_conjContinuousAlgEquiv_apply_apply, Submodule.coe_prodEquivOfClosedCompl_symm, ofSubmodules_apply, VectorField.mlieBracket_smul_right, 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, Bundle.Trivialization.continuousLinearEquivAt_prod, coe_prodCongr, Continuous.prod_map_equivL, 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	15 math math: conjContinuousAlgEquiv_refl, Bundle.Trivial.continuousLinearEquivAt_trivialization, ContinuousAlgEquiv.refl_toContinuousLinearEquiv, ContinuousAlgEquiv.coeCLE_refl, 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'
restrictScalars 📖	CompOp	3 math math: restrictScalars_symm_apply, restrictScalars_apply, restrictScalars_toLinearEquiv
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	—
toContinuousAddEquiv 📖	CompOp	1 math math: toContinuousAddEquiv_coe
toContinuousLinearMap 📖	CompOp	228 math math: antilipschitz, ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, isConformalMap_conj, LinearIsometryEquiv.hasStrictFDerivAt, LinearIsometryEquiv.comp_fderiv, Bundle.Trivialization.symm_continuousLinearEquivAt_eq', ContinuousLinearMap.HasRightInverse.comp_continuousLinearEquivalence, ContinuousLinearMap.HasRightInverse.continuousLinearEquivalence_comp, hasRightInverse, MDifferentiableAt.cle_arrowCongr, RCLike.conjCLE_norm, HasFDerivWithinAt.of_local_left_inverse, ContinuousAlgEquiv.toContinuousLinearMap_toContinuousLinearEquiv_eq, OpenPartialHomeomorph.hasStrictFDerivAt_symm, 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, MDifferentiable.cle_arrowCongr, Submodule.coe_orthogonalDecomposition_symm, MeasureTheory.charFunDual_pi', continuousAlternatingMapCongrLeftEquiv_apply, conjContinuousAlgEquiv_apply, hasLeftInverse, ContinuousLinearMap.inverse_equiv, HasMFDerivAt.smul, 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, ContMDiffFiberwiseLinear.locality_aux₂, toContinuousAffineEquiv_toContinuousAffineMap, ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp, MDifferentiableWithinAt.cle_arrowCongr, comp_right_fderiv, ContinuousLinearMap.ringInverse_equiv, Unitary.coe_symm_linearIsometryEquiv_apply, HasStrictFDerivAt.of_local_left_inverse, PiLp.hasFDerivAt_toLp, ContMDiffOn.coordChangeL, iteratedFDerivWithin_comp_right, LinearEquiv.coe_toContinuousLinearEquiv_symm, MDifferentiableOn.coordChangeL, coe_symm_comp_coe, ContMDiffOn.cle_arrowCongr, contMDiffAt_coordChangeL, eq_toContinuousLinearMap_symm_comp, coe_inj, MDifferentiableWithinAt.coordChangeL, Diffeomorph.mfderivToContinuousLinearEquiv_coe, Submodule.coe_orthogonalDecomposition, comp_coe, fromTangentSpace_mfderiv_smul', coe_prodCongr, HasFDerivAt.of_local_left_inverse, UpperHalfPlane.smulFDeriv_J_mul, 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, Complex.conjCLE_coe_toLinearMap, ImplicitFunctionData.hasStrictFDerivAt, ContinuousLinearMap.intrinsicStar_eq_comp, Submodule.sndL_comp_coe_orthogonalDecomposition, norm_symm_pos, Bundle.Trivialization.coordChangeL_prod, subsingleton_or_nnnorm_symm_pos, comp_hasFDerivWithinAt_iff, ApproximatesLinearOn.antilipschitz, LinearIsometryEquiv.coe_coe'', coe_injective, HasFDerivAtFilter.star, Complex.conjCLE_nnorm, Continuous.prod_map_equivL, MDifferentiableOn.cle_arrowCongr, 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, fromTangentSpace_mfderiv_smul, 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, HasStrictFDerivAt.approximates_deriv_on_open_nhds, 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', HasStrictFDerivAt.to_localInverse, MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv, arrowCongrEquiv_symm_apply, leftInverse_hasLeftInverse, MDifferentiableAt.coordChangeL, ApproximatesLinearOn.closedBall_subset_target, 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, ContMDiffFiberwiseLinear.locality_aux₁, 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, HasStrictFDerivAt.to_local_left_inverse, LinearIsometryEquiv.star_eq_symm, continuousAlternatingMapCongr_apply, RCLike.toContinuousLinearMap_complexLinearIsometryEquiv, mfderiv_smul, 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, ContMDiffWithinAt.cle_arrowCongr, 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, OpenPartialHomeomorph.hasFDerivAt_symm, MeasureTheory.charFunDual_eq_prod_iff', Bundle.Trivialization.coe_continuousLinearEquivAt_eq', arrowCongrSL_toLinearEquiv_symm_apply, ContMDiffAt.cle_arrowCongr, ContinuousOn.prod_map_equivL, continuousOn_coordChange, LinearIsometryEquiv.comp_fderiv', mem_contMDiffFiberwiseLinear_iff, ofSubmodule'_toContinuousLinearMap, ApproximatesLinearOn.to_inv, ContMDiff.cle_arrowCongr, LinearIsometryEquiv.comp_hasStrictFDerivAt_iff, ContMDiff.coordChangeL, norm_pos, comp_hasStrictFDerivAt_iff, mfderivWithin_eq, LinearIsometryEquiv.submoduleMap_apply_coe, PiLp.hasStrictFDerivAt_toLp, unitary.linearIsometryEquiv_coe_apply
toHomeomorph 📖	CompOp	3 math math: coe_toHomeomorph, coe_symm_toHomeomorph, toHomeomorph_symm
toLinearEquiv 📖	CompOp	38 math math: Pi.comul_eq_adjoint, toLinearEquiv_symm, ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_toLinearEquiv, instIsZLatticeComap, LinearEquiv.toLinearEquiv_toContinuousLinearEquiv_symm, restrictScalars_toLinearEquiv, Pi.counit_eq_adjoint, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, RCLike.conjCLE_coe, ClosedSubmodule.closure_map_eq_mapEquiv_closure, trans_toLinearEquiv, Complex.conjCLE_toLinearEquiv, ContinuousLinearMap.equivRange_symm_toLinearEquiv, coe_toLinearEquiv, LinearEquiv.toLinearEquiv_toContinuousLinearEquiv, toLinearEquiv_smul, continuous_invFun, coe_uniqueProd, prodAssoc_toLinearEquiv, prodProdProdComm_toLinearEquiv, LinearEquiv.canLiftContinuousLinearEquiv, ContinuousAlgEquiv.toContinuousLinearEquiv_toLinearEquiv_eq, ClosedSubmodule.mapEquiv_apply, 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, Bundle.Trivialization.coe_coordChangeL', arrowCongrSL_toLinearEquiv_symm_apply, prodComm_toLinearEquiv, ofSubmodule'_toContinuousLinearMap, coe_symm_toLinearEquiv
toUnit 📖	CompOp	—
trans 📖	CompOp	12 math math: symm_trans_apply, ContinuousAlgEquiv.trans_toContinuousLinearEquiv, conjContinuousAlgEquiv_trans, Bundle.Trivialization.comp_continuousLinearEquivAt_eq_coord_change, 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	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike equivOfInverse ContinuousLinearMap ContinuousLinearMap.funLike	—	—
equivOfRightInverse_symm_apply 📖	mathematical	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	DFunLike.coe ContinuousLinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule AddCommGroup.toAddCommMonoid 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 ContinuousLinearMap ContinuousLinearMap.funLike	—	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 Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toLinearMap DFunLike.coe ContinuousLinearEquiv RingHomInvPair.ids instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike equivLike equivOfRightInverse ContinuousLinearMap ContinuousLinearMap.funLike	—	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
restrictScalars_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike restrictScalars	—	RingHomInvPair.ids
restrictScalars_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike equivLike symm restrictScalars	—	RingHomInvPair.ids
restrictScalars_toLinearEquiv 📖	mathematical	—	toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids restrictScalars LinearEquiv.restrictScalars	—	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 Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toLinearMap DFunLike.coe ContinuousLinearEquiv RingHomInvPair.ids instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike equivLike equivOfRightInverse SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ContinuousLinearMap ContinuousLinearMap.funLike	—	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
toContinuousAddEquiv_coe 📖	mathematical	—	DFunLike.coe ContinuousAddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike ContinuousAddEquiv.instEquivLike toContinuousAddEquiv ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids equivLike	—	RingHomInvPair.ids
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	13 math math: ImplicitFunctionData.isInvertible_fderiv_prodFun, isInvertible_comp_equiv, ModelWithCorners.isInvertible_fderivWithin_extendCoordChange, isInvertible_zero_iff, isInvertible_equiv, IsInvertible.inverse, IsInvertible.comp, IsInvertible.of_isInvertible_inverse, 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	34 math math: IsInvertible.inverse_comp_of_right, IsInvertible.inverse_comp_of_left, inverse_equiv, contDiffAt_map_inverse, ringInverse_equiv, mfderivWithin_extChartAt_symm_inverse_apply, HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain, VectorField.mpullback_apply, IsInvertible.inverse_inverse, inverse_eq, IsInvertible.inverse, inverse_zero, ContDiffAt.hasStrictFDerivAt_implicitFunction, 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, VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, 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_zero 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.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.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 📖	mathematical	ContinuousLinearMap.IsInvertible ContinuousLinearMap.inverse	ContinuousLinearMap.IsInvertible	—	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 DFunLike.coe LinearEquiv AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike	—	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	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids SetLike.instMembership Submodule.setLike instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module DFunLike.coe 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