LinearIsometry

📁 Source: Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

Statistics

Metric	Count
Definitions LinearIsometry, apply, comp, equivRange, id, instFunLike, instInhabited, instMonoid, submoduleMap, toContinuousLinearMap, toLinearMap, LinearIsometryClass, LinearIsometryEquiv, apply, symm_apply, instCoeFun, instCoeTCContinuousLinearEquiv, instCoeTCContinuousLinearMap, instEquivLike, instGroup, instInhabited, neg, ofBounds, ofEq, ofLinearIsometry, ofSurjective, ofTop, prodAssoc, prodComm, refl, submoduleMap, toContinuousLinearEquiv, toHomeomorph, toIsometryEquiv, toLinearEquiv, toLinearIsometry, trans, ulift, LinearIsometryEquivClass, toLinearIsometry, opLinearIsometryEquiv, SemilinearIsometryClass, SemilinearIsometryEquivClass, subtypeₗᵢ, «term_→ₗᵢ[_]_», «term_→ₗᵢ⋆[_]_», «term_→ₛₗᵢ[_]_», «term_≃ₗᵢ[_]_», «term_≃ₗᵢ⋆[_]_», «term_≃ₛₗᵢ[_]_»	50
Theorems antilipschitz, coe_comp, coe_id, coe_injective, coe_mk, coe_mul, coe_one, coe_pow, coe_toContinuousLinearMap, coe_toLinearMap, comp_assoc, comp_continuous_iff, comp_id, completeSpace_map, continuous, diam_image, diam_range, dist_map, ediam_image, ediam_range, edist_map, enorm_map, equivRange_apply_coe, ext, ext_iff, id_apply, id_comp, id_toContinuousLinearMap, id_toLinearMap, injective, instSemilinearIsometryClass, isComplete_image_iff, isComplete_image_iff', isComplete_map_iff, isComplete_map_iff', isEmbedding, isometry, lipschitz, map_add, map_eq_iff, map_ne, map_neg, map_smul, map_smulₛₗ, map_sub, map_zero, mul_def, nnnorm_map, norm_map, norm_map', one_def, preimage_ball, preimage_closedBall, preimage_sphere, submoduleMap_apply_coe, toContinuousLinearMap_inj, toContinuousLinearMap_injective, toLinearMap_inj, toLinearMap_injective, antilipschitz, apply_symm_apply, bijective, coe_coe, coe_coe'', coe_injective, coe_inv, coe_mk, coe_mul, coe_neg, coe_ofEq_apply, coe_ofLinearIsometry, coe_ofLinearIsometry_symm, coe_ofSurjective, coe_one, coe_prodAssoc, coe_prodAssoc_symm, coe_refl, coe_symm_toContinuousLinearEquiv, coe_symm_toHomeomorph, coe_symm_toIsometryEquiv, coe_symm_toLinearEquiv, coe_symm_trans, coe_toContinuousLinearEquiv, coe_toHomeomorph, coe_toIsometryEquiv, coe_toLinearEquiv, coe_toLinearIsometry, coe_trans, comp_continuousOn_iff, comp_continuous_iff, completeSpace_map, congr_arg, congr_fun, continuous, continuousAt, continuousOn, continuousWithinAt, diam_image, dist_map, ediam_image, edist_map, ext, ext_iff, image_ball, image_closedBall, image_eq_preimage_symm, image_sphere, injective, instSemilinearIsometryEquivClass, inv_def, isometry, lipschitz, map_add, map_eq_iff, map_eq_zero_iff, map_ne, map_smul, map_smulₛₗ, map_sub, map_zero, mul_def, mul_refl, nnnorm_map, norm_map, norm_map', ofEq_rfl, ofEq_symm, ofTop_apply, ofTop_symm_apply_coe, ofTop_toLinearEquiv, one_def, one_trans, preimage_ball, preimage_closedBall, preimage_sphere, prodComm_apply, prodComm_symm_apply, range_eq_univ, refl_mul, refl_trans, self_comp_symm, self_trans_symm, submoduleMap_apply_coe, submoduleMap_symm_apply_coe, surjective, symm_apply_apply, symm_bijective, symm_comp_self, symm_neg, symm_prodComm, symm_symm, symm_trans, symm_trans_self, toContinuousLinearEquiv_inj, toContinuousLinearEquiv_injective, toContinuousLinearEquiv_refl, toContinuousLinearEquiv_symm, toContinuousLinearEquiv_trans, toContinuousLinearMap_toLinearIsometry, toHomeomorph_inj, toHomeomorph_injective, toHomeomorph_symm, toHomeomorph_trans, toIsometryEquiv_inj, toIsometryEquiv_injective, toIsometryEquiv_symm, toIsometryEquiv_trans, toLinearEquiv_inj, toLinearEquiv_injective, toLinearEquiv_symm, toLinearEquiv_trans, toLinearIsometry_inj, toLinearIsometry_injective, trans_apply, trans_assoc, trans_one, trans_refl, ext_linearIsometry, ext_linearIsometryEquiv, isometry_opLinearEquiv, opLinearIsometryEquiv_apply, opLinearIsometryEquiv_symm_apply, toContinuousLinearEquiv_opLinearIsometryEquiv, toLinearEquiv_opLinearIsometryEquiv, antilipschitz, continuous, diam_image, diam_range, ediam_image, ediam_range, isometry, lipschitz, nnnorm_map, norm_map, toContinuousSemilinearMapClass, toSemilinearMapClass, norm_map, toSemilinearEquivClass, toSemilinearIsometryClass, coe_subtypeₗᵢ, subtypeₗᵢ_toContinuousLinearMap, subtypeₗᵢ_toLinearMap	202
Total	252

LinearIsometry

Definitions

Name	Category	Theorems
comp 📖	CompOp	5 math math: mul_def, coe_comp, comp_id, comp_assoc, id_comp
equivRange 📖	CompOp	1 math math: equivRange_apply_coe
id 📖	CompOp	10 math math: one_def, rTensor_def, id_toContinuousLinearMap, TensorProduct.mapIsometry_id_id, id_apply, id_toLinearMap, coe_id, comp_id, lTensor_def, id_comp
instFunLike 📖	CompOp	114 math math: TensorProduct.mapInclIsometry_apply, coe_toLinearMap, IsHilbertSum.surjective_isometry, OrthogonalFamily.linearIsometry_apply_single, lipschitz, diam_image, RCLike.ofRealLI_apply, map_smul, Complex.ofRealLI_apply, isComplete_image_iff', coe_toLinearIsometryEquiv, norm_map, IsHilbertSum.linearIsometryEquiv_symm_apply, OrthogonalFamily.orthonormal_sigma_orthonormal, map_add, isEmbedding, map_starProjection', coe_toContinuousLinearMap, OrthogonalFamily.norm_sq_diff_sum, IsHilbertSum.hasSum_linearIsometryEquiv_symm, preimage_closedBall, coe_one, InnerProductSpace.toDualMap_apply_apply, ext_iff, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, enorm_map, map_sub, edist_map, id_apply, equivRange_apply_coe, inner_map_map, lTensor_apply, MeasureTheory.Lp.compMeasurePreservingₗᵢ_apply_coe, InnerProductSpace.toDualMap_apply, extend_apply, ContinuousAlternatingMap.toContinuousMultilinearMapLI_apply, Submodule.IsOrtho.map, LinearIsometryEquiv.coe_ofLinearIsometry, ediam_image, coe_pow, dist_map, norm_iteratedFDeriv_comp_left, Submodule.HasOrthogonalProjection.map_linearIsometryEquiv', toSpanSingleton_apply, OrthogonalFamily.hasSum_linearIsometry, continuous, AffineIsometry.map_vsub, OrthogonalFamily.summable_of_lp, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, preimage_ball, ContinuousLinearMap.coe_restrictScalarsIsometry, injective, map_neg, map_smulₛₗ, norm_iteratedFDerivWithin_comp_left, Submodule.coe_subtypeₗᵢ, inr_apply, orthonormal_comp_iff, LinearIsometryEquiv.coe_toLinearIsometry, OrthogonalFamily.inner_sum, coe_injective, map_starProjection, coe_id, preimage_sphere, coe_toAffineIsometry, comp_continuous_iff, ContinuousAlternatingMap.restrictScalarsLI_apply, UniformSpace.Completion.coe_toComplₗᵢ, isometry, integral_comp_comm, StrictConvex.linearIsometry_preimage, antilipschitz, OrthogonalFamily.eq_ite, coe_comp, diam_range, LinearMap.coe_isometryOfInner, InnerProductSpace.toDual_apply_eq_toDualMap_apply, map_eq_iff, AffineIsometry.map_vadd, MeasureTheory.charFun_eq_charFunDual_toDualMap, completeSpace_map, MeasureTheory.withDensitySMulLI_apply, LinearMap.coe_isometryOfOrthonormal, TensorProduct.mapIsometry_apply, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, contDiff, strictConvexSpace_range_iff, coe_mul, inl_apply, ediam_range, ContinuousAlternatingMap.curryLeftLI_apply, OrthogonalFamily.norm_sum, strictConvexSpace_range, map_zero, IsHilbertSum.linearIsometryEquiv_symm_apply_single, nnnorm_map, withLpProdMap_apply, coe_mk, toLinearIsometryEquiv_apply, rTensor_apply, EuclideanGeometry.Sphere.secondInter_map, OrthogonalFamily.linearIsometry_apply, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, OrthogonalFamily.summable_iff_norm_sq_summable, Orientation.rotationAux_apply, instSemilinearIsometryClass, Submodule.IsOrtho.comap, submoduleMap_apply_coe, OrthogonalFamily.inner_right_fintype, angle_map, ContinuousLinearMap.coe_mulₗᵢ, OrthogonalFamily.inner_right_dfinsupp, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, Orthonormal.comp_linearIsometry
instInhabited 📖	CompOp	—
instMonoid 📖	CompOp	5 math math: one_def, coe_one, mul_def, coe_pow, coe_mul
submoduleMap 📖	CompOp	1 math math: submoduleMap_apply_coe
toContinuousLinearMap 📖	CompOp	19 math math: norm_compContinuousAlternatingMap, nnnorm_toContinuousLinearMap, ContinuousLinearMap.opNorm_comp_linearIsometryEquiv, Submodule.subtypeₗᵢ_toContinuousLinearMap, id_toContinuousLinearMap, coe_toContinuousLinearMap, ContinuousMultilinearMap.norm_compContinuous_linearIsometry_le, norm_toContinuousLinearMap, norm_compContinuousMultilinearMap, isConformalMap, FormalMultilinearSeries.le_radius_compContinuousLinearMap, FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq, norm_toContinuousLinearMap_comp, enorm_toContinuousLinearMap, InnerProductSpace.toContinuousLinearMap_toDualMap, LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry, toContinuousLinearMap_injective, norm_toContinuousLinearMap_le, toContinuousLinearMap_inj
toLinearMap 📖	CompOp	31 math math: coe_toLinearMap, toAffineIsometry_toAffineMap, Submodule.subtypeₗᵢ_toLinearMap, isComplete_map_iff, equivRange_apply_coe, lTensor_apply, AffineIsometry.linear_eq_linearIsometry, id_toLinearMap, LinearMap.isometryOfInner_toLinearMap, TensorProduct.nnnorm_map, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, coe_toSpanSingleton, toLinearMap_injective, map_starProjection, toLinearMap_inj, toLinearMap_rTensor, ContinuousLinearMap.restrictScalarsIsometry_toLinearMap, OrthogonalFamily.range_linearIsometry, TensorProduct.mapIsometry_apply, TensorProduct.toLinearMap_mapIsometry, TensorProduct.enorm_map, norm_map', Submodule.map_orthogonal, TensorProduct.norm_map, isComplete_map_iff', LinearMap.isometryOfOrthonormal_toLinearMap, rTensor_apply, toLinearMap_lTensor, submoduleMap_apply_coe, TensorProduct.inner_map_map, TensorProduct.toLinearMap_mapInclIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz 📖	mathematical	—	AntilipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal instOneNNReal DFunLike.coe LinearIsometry instFunLike	—	Isometry.antilipschitz isometry
coe_comp 📖	mathematical	—	DFunLike.coe LinearIsometry instFunLike comp	—	—
coe_id 📖	mathematical	—	DFunLike.coe LinearIsometry RingHom.id Semiring.toNonAssocSemiring instFunLike id	—	—
coe_injective 📖	mathematical	—	LinearIsometry DFunLike.coe instFunLike	—	—
coe_mk 📖	mathematical	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe LinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup LinearMap.instFunLike	LinearIsometry instFunLike	—	—
coe_mul 📖	mathematical	—	DFunLike.coe LinearIsometry RingHom.id Semiring.toNonAssocSemiring instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
coe_one 📖	mathematical	—	DFunLike.coe LinearIsometry RingHom.id Semiring.toNonAssocSemiring instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
coe_pow 📖	mathematical	—	DFunLike.coe LinearIsometry RingHom.id Semiring.toNonAssocSemiring instFunLike Monoid.toNatPow instMonoid Nat.iterate	—	hom_coe_pow
coe_toContinuousLinearMap 📖	mathematical	—	DFunLike.coe ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike toContinuousLinearMap LinearIsometry instFunLike	—	—
coe_toLinearMap 📖	mathematical	—	DFunLike.coe LinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup LinearMap.instFunLike toLinearMap LinearIsometry instFunLike	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_continuous_iff 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometry instFunLike	—	Isometry.comp_continuous_iff isometry
comp_id 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids id	—	ext RingHomCompTriple.ids
completeSpace_map 📖	mathematical	—	CompleteSpace Submodule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.map SemilinearMapClass.semilinearMap LinearIsometry instFunLike SemilinearIsometryClass.toSemilinearMapClass instSemilinearIsometryClass instUniformSpaceSubtype PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	IsComplete.completeSpace_coe isComplete_map_iff completeSpace_coe_iff_isComplete
continuous 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometry instFunLike	—	Isometry.continuous isometry
diam_image 📖	mathematical	—	Metric.diam SeminormedAddCommGroup.toPseudoMetricSpace Set.image DFunLike.coe LinearIsometry instFunLike	—	Isometry.diam_image isometry
diam_range 📖	mathematical	—	Metric.diam SeminormedAddCommGroup.toPseudoMetricSpace Set.range DFunLike.coe LinearIsometry instFunLike Set.univ	—	Isometry.diam_range isometry
dist_map 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometry instFunLike	—	Isometry.dist_eq isometry
ediam_image 📖	mathematical	—	Metric.ediam PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.image DFunLike.coe LinearIsometry instFunLike	—	Isometry.ediam_image isometry
ediam_range 📖	mathematical	—	Metric.ediam PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.range DFunLike.coe LinearIsometry instFunLike Set.univ	—	Isometry.ediam_range isometry
edist_map 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometry instFunLike	—	Isometry.edist_eq isometry
enorm_map 📖	mathematical	—	ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe LinearIsometry instFunLike	—	nnnorm_map
equivRange_apply_coe 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike LinearMap.range NormedAddCommGroup.toSeminormedAddCommGroup RingHomSurjective.invPair toLinearMap DFunLike.coe LinearIsometryEquiv Submodule.seminormedAddCommGroup Submodule.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike equivRange LinearIsometry instFunLike	—	RingHomSurjective.invPair
ext 📖	—	DFunLike.coe LinearIsometry instFunLike	—	—	coe_injective
ext_iff 📖	mathematical	—	DFunLike.coe LinearIsometry instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe LinearIsometry RingHom.id Semiring.toNonAssocSemiring instFunLike id	—	—
id_comp 📖	mathematical	—	comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.right_ids id	—	ext RingHomCompTriple.right_ids
id_toContinuousLinearMap 📖	mathematical	—	toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring id ContinuousLinearMap.id UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—
id_toLinearMap 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring id LinearMap.id AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—
injective 📖	mathematical	—	DFunLike.coe LinearIsometry NormedAddCommGroup.toSeminormedAddCommGroup instFunLike	—	Isometry.injective isometry
instSemilinearIsometryClass 📖	mathematical	—	SemilinearIsometryClass LinearIsometry instFunLike	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass norm_map'
isComplete_image_iff 📖	mathematical	—	IsComplete PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.image DFunLike.coe	—	isComplete_image_iff Isometry.isUniformInducing SemilinearIsometryClass.isometry
isComplete_image_iff' 📖	mathematical	—	IsComplete PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.image DFunLike.coe LinearIsometry instFunLike	—	isComplete_image_iff instSemilinearIsometryClass
isComplete_map_iff 📖	mathematical	—	IsComplete PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SetLike.coe Submodule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Submodule.setLike Submodule.map toLinearMap	—	isComplete_image_iff instSemilinearIsometryClass
isComplete_map_iff' 📖	mathematical	—	IsComplete PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SetLike.coe Submodule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Submodule.setLike Submodule.map toLinearMap	—	isComplete_map_iff
isEmbedding 📖	mathematical	—	Topology.IsEmbedding UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometry instFunLike	—	Isometry.isEmbedding isometry
isometry 📖	mathematical	—	Isometry PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometry instFunLike	—	AddMonoidHomClass.isometry_of_norm DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass norm_map
lipschitz 📖	mathematical	—	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal instOneNNReal DFunLike.coe LinearIsometry instFunLike	—	Isometry.lipschitz isometry
map_add 📖	mathematical	—	DFunLike.coe LinearIsometry instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	LinearMap.map_add
map_eq_iff 📖	mathematical	—	DFunLike.coe LinearIsometry NormedAddCommGroup.toSeminormedAddCommGroup instFunLike	—	injective
map_ne 📖	—	—	—	—	injective
map_neg 📖	mathematical	—	DFunLike.coe LinearIsometry instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	LinearMap.map_neg
map_smul 📖	mathematical	—	DFunLike.coe LinearIsometry RingHom.id Semiring.toNonAssocSemiring instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	LinearMap.map_smul
map_smulₛₗ 📖	mathematical	—	DFunLike.coe LinearIsometry instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	LinearMap.map_smulₛₗ
map_sub 📖	mathematical	—	DFunLike.coe LinearIsometry instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	LinearMap.map_sub
map_zero 📖	mathematical	—	DFunLike.coe LinearIsometry instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	LinearMap.map_zero
mul_def 📖	mathematical	—	LinearIsometry RingHom.id Semiring.toNonAssocSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid comp RingHomCompTriple.ids	—	—
nnnorm_map 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe LinearIsometry instFunLike	—	NNReal.eq norm_map
norm_map 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe LinearIsometry instFunLike	—	SemilinearIsometryClass.norm_map instSemilinearIsometryClass
norm_map' 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe LinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup LinearMap.instFunLike toLinearMap	—	—
one_def 📖	mathematical	—	LinearIsometry RingHom.id Semiring.toNonAssocSemiring MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid id	—	—
preimage_ball 📖	mathematical	—	Set.preimage DFunLike.coe LinearIsometry instFunLike Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace	—	Isometry.preimage_ball isometry
preimage_closedBall 📖	mathematical	—	Set.preimage DFunLike.coe LinearIsometry instFunLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace	—	Isometry.preimage_closedBall isometry
preimage_sphere 📖	mathematical	—	Set.preimage DFunLike.coe LinearIsometry instFunLike Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace	—	Isometry.preimage_sphere isometry
submoduleMap_apply_coe 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids toLinearMap DFunLike.coe LinearIsometry SemilinearMapClass.semilinearMap instFunLike SemilinearIsometryClass.toSemilinearMapClass instSemilinearIsometryClass Submodule.seminormedAddCommGroup Submodule.module submoduleMap	—	RingHomSurjective.ids SemilinearIsometryClass.toSemilinearMapClass instSemilinearIsometryClass
toContinuousLinearMap_inj 📖	mathematical	—	toContinuousLinearMap	—	toContinuousLinearMap_injective
toContinuousLinearMap_injective 📖	mathematical	—	LinearIsometry ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup toContinuousLinearMap	—	coe_injective
toLinearMap_inj 📖	mathematical	—	toLinearMap	—	toLinearMap_injective
toLinearMap_injective 📖	mathematical	—	LinearIsometry LinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup toLinearMap	—	—

LinearIsometry.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

LinearIsometryEquiv

Definitions

Name	Category	Theorems
instCoeFun 📖	CompOp	—
instCoeTCContinuousLinearEquiv 📖	CompOp	—
instCoeTCContinuousLinearMap 📖	CompOp	—
instEquivLike 📖	CompOp	477 math math: OrthonormalBasis.singleton_repr, LinearMap.IsSymmetric.clm_adjoint_eq, DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, strictConvex_preimage, fderiv_iteratedFDeriv, Orientation.kahler_map_complex, hasStrictFDerivAt, comp_fderiv, coe_symm_toIsometryEquiv, surjective, analyticOnNhd, hasFDerivAt_iff_hasGradientAt, coe_ofLinearIsometry_symm, Orientation.inner_rotation_pi_div_two_right_smul, Orientation.oangle_add_left_smul_rotation_pi_div_two, Real.fourierIntegral_comp_linearIsometry, Submodule.orthogonalDecomposition_symm_apply, IsometryEquiv.toRealLinearIsometryEquiv_symm_apply, hasFTaylorSeriesUpToOn_top_iff_right, Orientation.tan_oangle_add_left_smul_rotation_pi_div_two, LinearIsometry.coe_toLinearIsometryEquiv, Orientation.rotation_eq_self_iff, Submodule.reflection_orthogonal_apply, LinearMap.IsSymmetric.diagonalization_apply_self_apply, comp_fderivWithin, antilipschitz, ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries, iteratedFDerivWithin_succ_eq_comp_right, fderivWithin, HasFTaylorSeriesUpTo.hasFDerivAt, Orientation.neg_rotation, LinearMap.adjoint_eq_toCLM_adjoint, Orientation.eq_rotation_self_iff_angle_eq_zero, IsometryEquiv.toRealLinearIsometryEquiv_apply, range_eq_univ, InnerProductSpace.toDual_symm_apply, IsHilbertSum.linearIsometryEquiv_symm_apply, Orientation.tan_oangle_add_right_smul_rotation_pi_div_two, ext_iff, Complex.conjLIE_apply, coe_symm_toHomeomorph, MeasureTheory.charFun_toDual_symm_eq_charFunDual, coe_mk, ContinuousAlternatingMap.piLIE_apply_apply, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, ContinuousLinearMap.adjoint_id, iteratedFDerivWithin_succ_eq_comp_left, ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, norm_map, map_zero, apply_symm_apply, coe_toAffineIsometryEquiv, OrthonormalBasis.repr_self, ContinuousLinearMap.eq_adjoint_iff, Orientation.volumeForm_map, rotation_apply, piLpCongrRight_apply, Submodule.reflection_singleton_apply, HasFTaylorSeriesUpToOn.zero_eq', Orientation.inner_rightAngleRotation_swap', IsSelfAdjoint.adjoint_eq, OrthonormalBasis.measurePreserving_repr, Submodule.reflection_apply, lTensor_apply, EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint, ContinuousLinearMap.isPositive_self_comp_adjoint, LinearMap.adjoint_toContinuousLinearMap, coe_neg, image_eq_preimage_symm, adjoint_eq_symm, Orientation.neg_rotation_neg_pi_div_two, IsHilbertSum.hasSum_linearIsometryEquiv_symm, ContinuousAlternatingMap.constOfIsEmptyLIE_apply, LinearEquiv.coe_isometryOfOrthonormal, inner_map_eq_flip, Quaternion.linearIsometryEquivTuple_symm_apply, ContinuousAlternatingMap.ofSubsingletonLIE_symm_apply, fderiv, measurePreserving, coe_toLinearEquiv, Orientation.rotation_pi_apply, Orientation.rotation_rotation, coe_toHomeomorph, Orientation.rotation_map_complex, TensorProduct.lidIsometry_apply, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, Module.Basis.coe_toOrthonormalBasis_repr, map_add, AffineIsometryEquiv.map_vsub, Orientation.kahler_comp_rightAngleRotation, coe_ofEq_apply, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, hasGradientWithinAt_iff_hasFDerivWithinAt, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left, smul_apply, coe_injective, contDiff, ContinuousMultilinearMap.curryFinFinset_symm_apply_const, HasFPowerSeriesOnBall.fderiv_eq, coe_trans, comp_hasFDerivWithinAt_iff', piLpCongrLeft_apply, HasFTaylorSeriesUpToOn.hasFDerivWithinAt, OrthonormalBasis.coe_ofRepr, Submodule.adjoint_subtypeL, LinearIsometry.equivRange_apply_coe, RCLike.conjLIE_apply, Submodule.reflection_orthogonalComplement_singleton_eq_neg, Complex.orthonormalBasisOneI_repr_apply, coe_toContinuousLinearEquiv, Real.fourierIntegralInv_comp_linearIsometry, Orientation.rotation_map, Orientation.oangle_rotation_left, EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, HasFPowerSeriesWithinAt.fderivWithin_eq, ContinuousLinearMap.IsPositive.conj_adjoint, diam_image, InnerProductSpace.adjoint_rankOne, ofTop_symm_apply_coe, HilbertBasis.hasSum_repr, HasFDerivWithinAt.hasGradientWithinAt, Real.fourier_comp_linearIsometry, LinearMap.IsSymmetric.diagonalization_symm_apply, PiTensorProduct.liftIsometry_tprodL, coe_toMeasurableEquiv, image_sphere, nnnorm_map, InnerProductSpace.toDual_apply, OrthonormalBasis.tensorProduct_repr_tmul_apply', Real.fourierInv_comp_linearIsometry, iteratedFDerivWithin_eq_equiv_comp, MeasureTheory.integrable_comp, map_eq_iff, ContinuousLinearMap.adjoint_inner_left, Orientation.oangle_rotation_oangle_right, coe_prodAssoc_symm, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right, ContinuousMultilinearMap.ofSubsingletonₗᵢ_symm_apply, preimage_ball, continuousMultilinearCurryFin0_symm_apply, ContinuousAlternatingMap.ofSubsingletonLIE_apply, continuousMultilinearCurryRightEquiv_symm_apply, OrthonormalBasis.equiv_apply, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, ContinuousMap.linearIsometryBoundedOfCompact_symm_apply, congr_arg, Module.Basis.coe_toOrthonormalBasis_repr_symm, InnerProductSpace.toDual_apply_apply, ContinuousLinearMap.adjointAux_apply, Orientation.inner_rotation_pi_div_two_right, coe_lpBCFₗᵢ, ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self, comp_differentiableOn_iff, comp_differentiableAt_iff, Orientation.oangle_rotation, ContinuousLinearMap.coe_flipₗᵢ', OrthonormalBasis.repr_apply_apply, ContinuousAlternatingMap.constOfIsEmptyLIE_symm_apply, Orientation.inner_rotation_pi_div_two_left, LinearEquiv.extendOfIsometry_symm_eq, ContinuousMap.toLp_def, ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker, Orientation.oangle_rotation_self_left, ContinuousMultilinearMap.prodL_apply, hasFTaylorSeriesUpToOn_succ_iff_right, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, coe_toIsometryEquiv, piLpCurry_apply, Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero, coe_ofLinearIsometry, LinearMap.toMatrix_innerₛₗ_apply, ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff, Orientation.inner_rotation_pi_div_two_left_smul, LinearEquiv.extendOfIsometry_symm_apply, image_ball, Submodule.reflection_mem_subspace_orthogonal_precomplement_eq_neg, fderivWithin_iteratedFDerivWithin, Orientation.eq_rotation_self_iff, piLpCongrRight_single, Submodule.fst_orthogonalDecomposition_apply, dist_map, Orientation.inner_comp_rightAngleRotation, continuousWithinAt, ContinuousMultilinearMap.curryFinFinset_apply_const, norm_iteratedFDerivWithin_comp_left, inner_map_complex, HasGradientAt.hasFDerivAt, Submodule.reflection_reflection, hasFTaylorSeriesUpTo_succ_nat_iff_right, coe_symm_toLinearEquiv, Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero, EuclideanGeometry.reflection_apply_of_mem, Orthonormal.linearIsometryEquiv_symm_apply_single_one, iteratedFDeriv_eq_equiv_comp, hasFTaylorSeriesUpToOn_succ_nat_iff_right, Orientation.oangle_rotation_oangle_left, ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense, analyticWithinAt, toSpanUnitSingleton_apply, Submodule.starProjection_map_apply, coe_coe, HasFPowerSeriesAt.fderiv_eq, continuousMultilinearCurryFin0_apply, EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, Orientation.rightAngleRotation_rightAngleRotation, IsSelfAdjoint.conj_adjoint, ContinuousMultilinearMap.curryMidEquiv_apply, Orientation.areaForm_comp_linearIsometryEquiv, ofTop_apply, comp_differentiableWithinAt_iff, withLpProdCongr_symm_apply, Submodule.reflection_sub, LinearEquiv.extendOfIsometry_apply, Orientation.rotation_eq_self_iff_angle_eq_zero, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, LinearEquiv.coe_isometryOfInner, Orientation.oangle_rotation_right, starₗᵢ_apply, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, analyticOn, analyticAt, EuclideanSpace.basisFun_repr, HasFTaylorSeriesUpToOn.hasFDerivAt, RCLike.realLinearIsometryEquiv_symm_apply, Orientation.oangle_sub_right_smul_rotation_pi_div_two, ContinuousLinearMap.isSelfAdjoint_iff', OrthonormalBasis.equiv_apply_euclideanSpace, Complex.orthonormalBasisOneI_repr_symm_apply, symm_comp_self, iteratedDeriv_eq_equiv_comp, HasFTaylorSeriesUpToOn.shift_of_succ, Orientation.areaForm_comp_rightAngleRotation, contDiffPointwiseHolderAt_left_comp, MeasureTheory.integral_comp, RCLike.complexLinearIsometryEquiv_symm_apply, coe_lpPiLpₗᵢ, coe_coe'', Orientation.inner_rightAngleRotation_left, coe_toLinearIsometry, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left, coe_withLpProdUnique, OrthonormalBasis.map_apply, trans_apply, OrthonormalBasis.sum_repr_symm, Orientation.inner_smul_rotation_pi_div_two_right, IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero, strictConvex_image, Orientation.kahler_rotation_left', ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const, edist_map, hasGradientAt_iff_hasFDerivAt, FormalMultilinearSeries.leftInv_coeff_one, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, TensorProduct.assocIsometry_apply, injective, MulOpposite.opLinearIsometryEquiv_symm_apply, hasFDerivAt, rTensor_apply, inner_map_map, Orientation.neg_rotation_pi_div_two, ContinuousAlternatingMap.piLIE_symm_apply_apply, HasFPowerSeriesAt.hasFDerivAt, OrthonormalBasis.measurePreserving_repr_symm, Orientation.linearIsometryEquiv_comp_rightAngleRotation, EuclideanSpace.piLpCongrLeft_single, norm_iteratedFDeriv_comp_right, Orientation.inner_rightAngleRotation_swap, piLpCurry_symm_apply, rotationOf_coe, coe_inv, Orientation.oangle_sub_left_smul_rotation_pi_div_two, Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero, map_sub, symm_conjStarAlgEquiv_apply_apply, Orientation.oangle_add_right_smul_rotation_pi_div_two, symm_apply_apply, Orientation.inner_smul_rotation_pi_div_two_left, isometry, submoduleMap_symm_apply_coe, InnerProductSpace.rankOne_comp, Orientation.kahler_rightAngleRotation_left, Orientation.kahler_comp_linearIsometryEquiv, InnerProductSpace.toMatrix_rankOne, PiTensorProduct.liftIsometry_comp_mapL, continuousMultilinearCurryLeftEquiv_apply, Orientation.kahler_rotation_left, PiTensorProduct.liftIsometry_symm_apply, iteratedFDeriv_succ_eq_comp_right, ContinuousLinearMap.adjoint_toSpanSingleton, coe_one, coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, coe_ofSurjective, Submodule.reflection_eq_self_iff, HasFPowerSeriesWithinOnBall.fderivWithin_eq, ContinuousMultilinearMap.piₗᵢ_symm_apply, HasFTaylorSeriesUpToOn.hasStrictFDerivAt, prodComm_symm_apply, coe_symm_toContinuousLinearEquiv, OrthonormalBasis.repr_symm_single, Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two, withLpProdCongr_apply, coe_starₗᵢ, InnerProductSpace.toDual_apply_eq_toDualMap_apply, Orientation.oangle_map, Submodule.reflection_map_apply, continuousAt, HasFPowerSeriesOnBall.hasFDerivAt, withLpProdUnique_symm_apply, toMatrix_innerSL_apply, OrthonormalBasis.equiv_apply_basis, self_comp_symm, ContinuousLinearMap.orthogonal_range, Orientation.kahler_map, comp_differentiable_iff, coe_refl, PiTensorProduct.liftIsometry_apply_apply, ContinuousMultilinearMap.prodL_symm_apply, ProbabilityTheory.covarianceBilin_map, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, Orientation.coe_basisRightAngleRotation, continuousOn, Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero, Orientation.areaForm_map, ContinuousMap.linearIsometryBoundedOfCompact_apply_apply, congr_fun, ContinuousLinearMap.adjoint_comp, iteratedFDeriv_zero_eq_comp, map_eq_zero_iff, HilbertBasis.repr_self, TensorProduct.commIsometry_apply, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', continuousMultilinearCurryRightEquiv_symm_apply', iteratedDerivWithin_eq_equiv_comp, Submodule.adjoint_orthogonalProjection, hasFDerivWithinAt_iff_hasGradientWithinAt, ContinuousAlternatingMap.prodLIE_apply, comp_hasFDerivAt_iff', PadicInt.mahlerEquiv_apply, Submodule.reflection_involutive, comp_continuousOn_iff, ContinuousLinearMap.IsPositive.adjoint_conj, Complex.isometryOfOrthonormal_apply, withLpProdUnique_apply, Orientation.areaForm_map_complex, MulOpposite.opLinearIsometryEquiv_apply, comp_hasFDerivAt_iff, ContinuousLinearMap.star_eq_adjoint, Orientation.inner_rightAngleRotation_right, ProperCone.hyperplane_separation_of_notMem, iteratedFDerivWithin_zero_eq_comp, Orientation.rotation_apply, ContinuousLinearMap.coe_flipₗᵢ, OrthonormalBasis.sum_repr, Submodule.reflection_mem_subspace_eq_self, IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero_symm, hasFDerivWithinAt, IsHilbertSum.linearIsometryEquiv_symm_apply_single, IsSelfAdjoint.adjoint_conj, AffineIsometryEquiv.map_vadd, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr, lipschitz, piLpCongrLeft_single, ContinuousLinearMap.adjoint_inner_right, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, symm_smul_apply, OrthonormalBasis.coe_toBasis_repr_apply, coe_symm_trans, OrthonormalBasis.coe_equiv_euclideanSpace, Orientation.rightAngleRotation_map, Orientation.kahler_rotation_right, continuousMultilinearCurryRightEquiv_apply', Orthonormal.comp_linearIsometryEquiv, HasFiniteFPowerSeriesOnBall.hasFDerivAt, HasFDerivAt.hasGradientAt, ContinuousLinearMap.isAdjointPair_inner, differentiableAt, differentiable, Submodule.snd_orthogonalDecomposition_apply, withLpProdComm_apply, LinearEquiv.extendOfIsometry_eq, Orientation.oangle_rotation_self_right, withLpProdAssoc_apply, continuousMultilinearCurryLeftEquiv_symm_apply, Submodule.orthogonalDecomposition_apply, iteratedFDeriv_succ_eq_comp_left, comp_hasFDerivWithinAt_iff, prodComm_apply, ContinuousMultilinearMap.piₗᵢ_apply, Orientation.areaForm_rightAngleRotation_right, ContinuousMultilinearMap.ofSubsingletonₗᵢ_apply, LinearIsometry.toLinearIsometryEquiv_apply, continuousMultilinearCurryFin1_symm_apply, instSemilinearIsometryEquivClass, PadicInt.mahlerEquiv_symm_apply, Orientation.inner_smul_rotation_pi_div_two_smul_left, comp_continuous_iff, Orientation.oangle_map_complex, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, map_smul, ContinuousLinearMap.norm_adjoint_comp_self, Orientation.inner_smul_rotation_pi_div_two_smul_right, Complex.rightAngleRotation, HasFTaylorSeriesUpTo.zero_eq', ContinuousMultilinearMap.curryFinFinset_symm_apply, Orientation.kahler_rightAngleRotation_right, Quaternion.linearIsometryEquivTuple_apply, ContinuousAffineMap.toConstProdContinuousLinearMap_fst, integrable_comp_iff, Complex.isometryOfOrthonormal_symm_apply, Orientation.inner_rightAngleRotation_self, HasFiniteFPowerSeriesOnBall.fderiv_eq, continuous, TensorProduct.congrIsometry_apply, HasFPowerSeriesAt.hasStrictFDerivAt, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right, ContinuousLinearMap.isPositive_adjoint_comp_self, continuousMultilinearCurryRightEquiv_apply, ContinuousAlternatingMap.prodLIE_symm_apply, HasFPowerSeriesWithinAt.hasFDerivWithinAt, norm_iteratedFDeriv_comp_left, Orientation.rotation_symm_apply, withLpUniqueProd_apply, coe_mul, HasGradientWithinAt.hasFDerivWithinAt, FormalMultilinearSeries.rightInv_coeff_one, Orientation.volumeForm_comp_linearIsometryEquiv, Pi.orthonormalBasis_repr, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, Orientation.rotation_oangle_eq_iff_norm_eq, ContinuousLinearMap.fpowerSeries_apply_one, ContinuousMultilinearMap.curryFinFinset_apply, differentiableOn, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, conjStarAlgEquiv_apply_apply, Orthonormal.equiv_apply, Orientation.rightAngleRotation_neg_orientation, Orientation.rotationAux_apply, withLpUniqueProd_symm_apply, HasFPowerSeriesWithinOnBall.hasFDerivWithinAt, OrthonormalBasis.repr_reindex, differentiableWithinAt, ContinuousLinearMap.adjoint_innerSL_apply, EuclideanGeometry.reflection_apply, comp_fderiv', RCLike.realLinearIsometryEquiv_apply, Orientation.rightAngleRotation_map_complex, Orientation.areaForm_rightAngleRotation_left, ContinuousLinearMap.fpowerSeriesBilinear_apply_one, OrthonormalBasis.tensorProduct_repr_tmul_apply, TensorProduct.assocIsometry_symm_apply, Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg, PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp, ContinuousLinearMap.innerSL_apply_comp, TensorProduct.lidIsometry_symm_apply, HilbertBasis.hasSum_repr_symm, comp_hasStrictFDerivAt_iff, withLpProdAssoc_symm_apply, ContinuousLinearMap.adjoint_adjoint, coe_prodAssoc, preimage_sphere, coe_withLpUniqueProd, image_closedBall, ContinuousLinearMap.orthogonal_ker, Complex.rotation, RCLike.complexLinearIsometryEquiv_apply, map_smulₛₗ, ContinuousAffineMap.toConstProdContinuousLinearMap_snd, ContinuousMultilinearMap.curryMidEquiv_symm_apply, ediam_image, bijective, submoduleMap_apply_coe, coe_symm_toMeasurableEquiv, preimage_closedBall, continuousMultilinearCurryFin1_apply
instGroup 📖	CompOp	32 math math: trans_one, Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, rotation_injective, rotation_apply, toMatrix_rotation, Unitary.coe_linearIsometryEquiv_apply, Unitary.linearIsometryEquiv_coe_apply, unitary.linearIsometryEquiv_coe_symm_apply, reflections_generate_dim_aux, Unitary.coe_symm_linearIsometryEquiv_apply, reflections_generate, Submodule.reflection_inv, linear_isometry_complex, Unitary.linearIsometryEquiv_coe_symm_apply, Submodule.reflection_mul_reflection, rotationOf_rotation, rotation_trans, coe_inv, coe_one, linearEquiv_det_rotation, mul_refl, reflections_generate_dim, det_rotation, rotation_symm, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, one_def, mul_def, inv_def, refl_mul, coe_mul, one_trans, unitary.linearIsometryEquiv_coe_apply
instInhabited 📖	CompOp	—
neg 📖	CompOp	10 math math: coe_neg, Orientation.rightAngleRotation_trans_rightAngleRotation, Orientation.rightAngleRotation_symm, SchwartzMap.fourierInv_apply_eq, AffineIsometryEquiv.symm_constVSub, Submodule.reflection_orthogonal, Submodule.reflection_bot, Orientation.rightAngleRotation_trans_neg_orientation, Orientation.rotation_pi, symm_neg
ofBounds 📖	CompOp	—
ofEq 📖	CompOp	3 math math: coe_ofEq_apply, ofEq_rfl, ofEq_symm
ofLinearIsometry 📖	CompOp	3 math math: coe_ofLinearIsometry_symm, Orientation.rightAngleRotation_def, coe_ofLinearIsometry
ofSurjective 📖	CompOp	1 math math: coe_ofSurjective
ofTop 📖	CompOp	3 math math: ofTop_toLinearEquiv, ofTop_symm_apply_coe, ofTop_apply
prodAssoc 📖	CompOp	2 math math: coe_prodAssoc_symm, coe_prodAssoc
prodComm 📖	CompOp	3 math math: symm_prodComm, prodComm_symm_apply, prodComm_apply
refl 📖	CompOp	20 math math: Submodule.reflection_trans_reflection, TensorProduct.congrIsometry_refl_refl, self_trans_symm, conjStarAlgEquiv_refl, Orientation.rotation_zero, OrthonormalBasis.equiv_self_rfl, symm_trans_self, piLpCongrRight_refl, linear_isometry_complex_aux, trans_refl, refl_trans, Orthonormal.equiv_refl, coe_refl, mul_refl, lTensor_def, toContinuousLinearEquiv_refl, one_def, ofEq_rfl, refl_mul, rTensor_def
submoduleMap 📖	CompOp	2 math math: submoduleMap_symm_apply_coe, submoduleMap_apply_coe
toContinuousLinearEquiv 📖	CompOp	50 math math: isConformalMap_conj, hasStrictFDerivAt, comp_fderiv, comp_fderivWithin, fderivWithin, conjStarAlgEquiv_apply, Unitary.coe_linearIsometryEquiv_apply, Unitary.linearIsometryEquiv_coe_apply, adjoint_eq_symm, Submodule.IsOrtho.map_iff, Submodule.coe_orthogonalDecomposition_symm, fderiv, comp_hasFDerivWithinAt_iff', unitary.linearIsometryEquiv_coe_symm_apply, ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp, coe_toContinuousLinearEquiv, toContinuousLinearEquiv_inj, Unitary.coe_symm_linearIsometryEquiv_apply, SchwartzMap.fourierInv_apply_eq, Submodule.coe_orthogonalDecomposition, completeSpace_map, Unitary.linearIsometryEquiv_coe_symm_apply, toContinuousLinearEquiv_symm, coe_coe, Submodule.sndL_comp_coe_orthogonalDecomposition, coe_coe'', hasFDerivAt, submoduleMap_symm_apply_coe, Submodule.IsOrtho.comap_iff, starₗᵢ_toContinuousLinearEquiv, coe_symm_toContinuousLinearEquiv, toContinuousLinearMap_toLinearIsometry, EuclideanGeometry.hasFDerivAt_inversion, comp_hasFDerivAt_iff', toContinuousLinearEquiv_refl, comp_hasFDerivAt_iff, toContinuousLinearEquiv_trans, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv, hasFDerivWithinAt, Submodule.fstL_comp_coe_orthogonalDecomposition, toContinuousLinearEquiv_injective, star_eq_symm, RCLike.toContinuousLinearMap_complexLinearIsometryEquiv, MulOpposite.toContinuousLinearEquiv_opLinearIsometryEquiv, comp_hasFDerivWithinAt_iff, toContinuousLinearEquiv_smul, comp_fderiv', comp_hasStrictFDerivAt_iff, submoduleMap_apply_coe, unitary.linearIsometryEquiv_coe_apply
toHomeomorph 📖	CompOp	6 math math: coe_symm_toHomeomorph, toHomeomorph_symm, coe_toHomeomorph, toHomeomorph_injective, toHomeomorph_inj, toHomeomorph_trans
toIsometryEquiv 📖	CompOp	7 math math: coe_symm_toIsometryEquiv, toIsometryEquiv_injective, coe_toIsometryEquiv, toIsometryEquiv_inj, toIsometryEquiv_trans, toIsometryEquiv_symm, ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv
toLinearEquiv 📖	CompOp	59 math math: Complex.linearEquiv_det_conjLIE, Submodule.toLinearEquiv_orthogonalDecomposition_symm, Orientation.linearEquiv_det_rotation, AffineIsometryEquiv.linear_eq_linear_isometry, Submodule.toLinearEquiv_orthogonalDecomposition, TensorProduct.toLinearEquiv_lidIsometry, Orientation.volumeForm_map, toMatrix_rotation, lTensor_apply, toLinearEquiv_symm, adjoint_toLinearMap_eq_symm, coe_toLinearEquiv, Orientation.det_rotation, Orientation.rotation_map, LinearEquiv.isometryOfOrthonormal_toLinearEquiv, ofTop_toLinearEquiv, OrthonormalBasis.toBasis_map, Submodule.map_orthogonal_equiv, Submodule.linearEquiv_det_reflection, LinearMap.isSymmetric_linearIsometryEquiv_conj_iff, ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv, TensorProduct.toLinearEquiv_congrIsometry, Orientation.rightAngleRotation_map', TensorProduct.toLinearEquiv_commIsometry, toLinearEquiv_injective, coe_symm_toLinearEquiv, LinearMap.isPositive_linearIsometryEquiv_conj_iff, Orthonormal.map_equiv, Submodule.starProjection_map_apply, MulOpposite.toLinearEquiv_opLinearIsometryEquiv, withLpProdCongr_symm_apply, toLinearEquiv_lTensor, toLinearEquiv_smul, Orthonormal.equiv_toLinearEquiv, toAffineIsometryEquiv_toAffineEquiv, Submodule.reflection_map, Submodule.det_reflection, LinearEquiv.isometryOfInner_toLinearEquiv, rTensor_apply, Orientation.rotation_eq_matrix_toLin, submoduleMap_symm_apply_coe, linearEquiv_det_rotation, Orientation.oangle_map, Submodule.reflection_map_apply, ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv, TensorProduct.toLinearEquiv_assocIsometry, Orientation.kahler_map, Orientation.areaForm_map, OrthonormalBasis.coe_toBasis_repr, Orthonormal.mapLinearIsometryEquiv, det_rotation, Orientation.rightAngleRotation_map, norm_map', toLinearEquiv_rTensor, Submodule.HasOrthogonalProjection.map_linearIsometryEquiv, toLinearEquiv_inj, Complex.det_conjLIE, submoduleMap_apply_coe, toLinearEquiv_trans
toLinearIsometry 📖	CompOp	11 math math: InnerProductSpace.toLinearIsometry_toDual, ContinuousLinearMap.opNorm_comp_linearIsometryEquiv, FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq, Submodule.HasOrthogonalProjection.map_linearIsometryEquiv', toLinearIsometry_injective, coe_toLinearIsometry, toContinuousLinearMap_toLinearIsometry, toAffineIsometryEquiv_toAffineIsometry, toLinearIsometry_rTensor, toLinearIsometry_lTensor, toLinearIsometry_inj
trans 📖	CompOp	32 math math: trans_one, Submodule.reflection_trans_reflection, trans_smul, Orientation.rightAngleRotation_trans_rightAngleRotation, coe_trans, self_trans_symm, Orientation.rightAngleRotation_symm, conjStarAlgEquiv_trans, Orientation.rightAngleRotation_map', Orthonormal.equiv_trans, linear_isometry_complex, symm_trans_self, Orientation.rotation_trans, trans_apply, Submodule.reflection_map, rotation_trans, Submodule.reflection_orthogonal, trans_assoc, trans_refl, symm_trans, refl_trans, Orientation.rightAngleRotation_trans_neg_orientation, smul_trans, toIsometryEquiv_trans, toContinuousLinearEquiv_trans, coe_symm_trans, toHomeomorph_trans, mul_def, Complex.map_isometryOfOrthonormal, Orientation.linearIsometryEquiv_comp_rightAngleRotation', one_trans, toLinearEquiv_trans
ulift 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz 📖	mathematical	—	AntilipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal instOneNNReal DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Isometry.antilipschitz isometry
apply_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike symm	—	LinearEquiv.apply_symm_apply
bijective 📖	mathematical	—	Function.Bijective DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	LinearEquiv.bijective
coe_coe 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike ContinuousLinearEquiv.equivLike toContinuousLinearEquiv LinearIsometryEquiv instEquivLike	—	—
coe_coe'' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike ContinuousLinearEquiv.toContinuousLinearMap toContinuousLinearEquiv LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	—
coe_injective 📖	mathematical	—	LinearIsometryEquiv DFunLike.coe EquivLike.toFunLike instEquivLike	—	DFunLike.coe_injective
coe_inv 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup symm	—	RingHomInvPair.ids
coe_mk 📖	mathematical	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe LinearEquiv AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	LinearIsometryEquiv instEquivLike	—	—
coe_mul 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup	—	RingHomInvPair.ids
coe_neg 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	RingHomInvPair.ids
coe_ofEq_apply 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule.seminormedAddCommGroup Submodule.module EquivLike.toFunLike instEquivLike ofEq	—	RingHomInvPair.ids
coe_ofLinearIsometry 📖	mathematical	LinearMap.comp AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ LinearIsometry.toLinearMap LinearMap.id	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike ofLinearIsometry LinearIsometry LinearIsometry.instFunLike	—	RingHomInvPair.triples₂
coe_ofLinearIsometry_symm 📖	mathematical	LinearMap.comp AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ LinearIsometry.toLinearMap LinearMap.id	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike symm ofLinearIsometry LinearMap LinearMap.instFunLike	—	RingHomInvPair.triples₂
coe_ofSurjective 📖	mathematical	DFunLike.coe LinearIsometry NormedAddCommGroup.toSeminormedAddCommGroup LinearIsometry.instFunLike	LinearIsometryEquiv EquivLike.toFunLike instEquivLike ofSurjective	—	—
coe_one 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup	—	RingHomInvPair.ids
coe_prodAssoc 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.seminormedAddCommGroup Prod.instModule Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike instEquivLike prodAssoc Equiv Equiv.instEquivLike Equiv.prodAssoc	—	RingHomInvPair.ids
coe_prodAssoc_symm 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.seminormedAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instAddCommMonoid EquivLike.toFunLike instEquivLike symm prodAssoc Equiv Equiv.instEquivLike Equiv.symm Equiv.prodAssoc	—	RingHomInvPair.ids
coe_refl 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike refl	—	RingHomInvPair.ids
coe_symm_toContinuousLinearEquiv 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm toContinuousLinearEquiv LinearIsometryEquiv instEquivLike symm	—	—
coe_symm_toHomeomorph 📖	mathematical	—	DFunLike.coe Homeomorph UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm toHomeomorph LinearIsometryEquiv instEquivLike symm	—	—
coe_symm_toIsometryEquiv 📖	mathematical	—	DFunLike.coe IsometryEquiv PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace EquivLike.toFunLike IsometryEquiv.instEquivLike IsometryEquiv.symm toIsometryEquiv LinearIsometryEquiv instEquivLike symm	—	—
coe_symm_toLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm toLinearEquiv LinearIsometryEquiv instEquivLike symm	—	—
coe_symm_trans 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike symm trans	—	—
coe_toContinuousLinearEquiv 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike ContinuousLinearEquiv.equivLike toContinuousLinearEquiv LinearIsometryEquiv instEquivLike	—	—
coe_toHomeomorph 📖	mathematical	—	DFunLike.coe Homeomorph UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike toHomeomorph LinearIsometryEquiv instEquivLike	—	—
coe_toIsometryEquiv 📖	mathematical	—	DFunLike.coe IsometryEquiv PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace EquivLike.toFunLike IsometryEquiv.instEquivLike toIsometryEquiv LinearIsometryEquiv instEquivLike	—	—
coe_toLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearEquiv LinearIsometryEquiv instEquivLike	—	—
coe_toLinearIsometry 📖	mathematical	—	DFunLike.coe LinearIsometry LinearIsometry.instFunLike toLinearIsometry LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	—
coe_trans 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike trans	—	—
comp_continuousOn_iff 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Isometry.comp_continuousOn_iff isometry
comp_continuous_iff 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Isometry.comp_continuous_iff isometry
completeSpace_map 📖	mathematical	—	CompleteSpace Submodule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.map RingHomSurjective.invPair ContinuousLinearMap.toLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearEquiv.toContinuousLinearMap toContinuousLinearEquiv instUniformSpaceSubtype	—	LinearIsometry.completeSpace_map RingHomSurjective.invPair
congr_arg 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	—
congr_fun 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	—
continuous 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Isometry.continuous isometry
continuousAt 📖	mathematical	—	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Continuous.continuousAt continuous
continuousOn 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Continuous.continuousOn continuous
continuousWithinAt 📖	mathematical	—	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Continuous.continuousWithinAt continuous
diam_image 📖	mathematical	—	Metric.diam SeminormedAddCommGroup.toPseudoMetricSpace Set.image DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Isometry.diam_image isometry
dist_map 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	LinearIsometry.dist_map
ediam_image 📖	mathematical	—	Metric.ediam PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.image DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Isometry.ediam_image isometry
edist_map 📖	mathematical	—	EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	LinearIsometry.edist_map
ext 📖	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	—	toLinearEquiv_injective LinearEquiv.ext
ext_iff 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	ext
image_ball 📖	mathematical	—	Set.image DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace	—	IsometryEquiv.image_ball
image_closedBall 📖	mathematical	—	Set.image DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace	—	IsometryEquiv.image_closedBall
image_eq_preimage_symm 📖	mathematical	—	Set.image DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike Set.preimage symm	—	LinearEquiv.image_eq_preimage_symm
image_sphere 📖	mathematical	—	Set.image DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace	—	IsometryEquiv.image_sphere
injective 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	LinearEquiv.injective
instSemilinearIsometryEquivClass 📖	mathematical	—	SemilinearIsometryEquivClass LinearIsometryEquiv instEquivLike	—	map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass norm_map'
inv_def 📖	mathematical	—	LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup symm	—	RingHomInvPair.ids
isometry 📖	mathematical	—	Isometry PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	LinearIsometry.isometry
lipschitz 📖	mathematical	—	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal instOneNNReal DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	Isometry.lipschitz isometry
map_add 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	LinearEquiv.map_add
map_eq_iff 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	injective
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	LinearEquiv.map_eq_zero_iff
map_ne 📖	—	—	—	—	injective
map_smul 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	RingHomInvPair.ids LinearEquiv.map_smul
map_smulₛₗ 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	LinearEquiv.map_smulₛₗ
map_sub 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	LinearMap.map_sub
map_zero 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	LinearEquiv.map_zero
mul_def 📖	mathematical	—	LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup trans RingHomCompTriple.ids	—	RingHomInvPair.ids
mul_refl 📖	mathematical	—	LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup refl	—	RingHomInvPair.ids refl_trans
nnnorm_map 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	SemilinearIsometryClass.nnnorm_map SemilinearIsometryEquivClass.toSemilinearIsometryClass instSemilinearIsometryEquivClass
norm_map 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	norm_map'
norm_map' 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe LinearEquiv AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearEquiv	—	—
ofEq_rfl 📖	mathematical	—	ofEq Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup refl SetLike.instMembership Submodule.setLike Submodule.seminormedAddCommGroup Submodule.module	—	RingHomInvPair.ids
ofEq_symm 📖	mathematical	—	symm Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule.seminormedAddCommGroup Submodule.module ofEq	—	RingHomInvPair.ids
ofTop_apply 📖	mathematical	Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Submodule.instTop	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids SetLike.instMembership Submodule.setLike Submodule.seminormedAddCommGroup Submodule.module EquivLike.toFunLike instEquivLike ofTop	—	RingHomInvPair.ids
ofTop_symm_apply_coe 📖	mathematical	Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Submodule.instTop	SetLike.instMembership Submodule.setLike DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule.seminormedAddCommGroup Submodule.module EquivLike.toFunLike instEquivLike symm ofTop	—	RingHomInvPair.ids
ofTop_toLinearEquiv 📖	mathematical	Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Submodule.instTop	toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids SetLike.instMembership Submodule.setLike Submodule.seminormedAddCommGroup Submodule.module ofTop LinearEquiv.ofTop	—	RingHomInvPair.ids
one_def 📖	mathematical	—	LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup refl	—	RingHomInvPair.ids
one_trans 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids RingHomCompTriple.right_ids LinearIsometryEquiv InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup	—	refl_trans
preimage_ball 📖	mathematical	—	Set.preimage DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace symm	—	IsometryEquiv.preimage_ball
preimage_closedBall 📖	mathematical	—	Set.preimage DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace symm	—	IsometryEquiv.preimage_closedBall
preimage_sphere 📖	mathematical	—	Set.preimage DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace symm	—	IsometryEquiv.preimage_sphere
prodComm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.seminormedAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike instEquivLike prodComm	—	RingHomInvPair.ids
prodComm_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.seminormedAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike instEquivLike symm prodComm	—	RingHomInvPair.ids
range_eq_univ 📖	mathematical	—	Set.range DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike Set.univ	—	coe_toIsometryEquiv IsometryEquiv.range_eq_univ
refl_mul 📖	mathematical	—	LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup refl	—	RingHomInvPair.ids trans_refl
refl_trans 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids RingHomCompTriple.right_ids refl	—	ext RingHomInvPair.ids RingHomCompTriple.ids RingHomCompTriple.right_ids
self_comp_symm 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike symm	—	symm_comp_self
self_trans_symm 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomInvPair.triples₂ symm refl	—	ext RingHomInvPair.ids RingHomInvPair.triples₂ symm_apply_apply
submoduleMap_apply_coe 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.map RingHomSurjective.invPair LinearEquiv.toLinearMap toLinearEquiv DFunLike.coe LinearIsometryEquiv ContinuousLinearMap.toLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearEquiv.toContinuousLinearMap toContinuousLinearEquiv Submodule.seminormedAddCommGroup Submodule.module EquivLike.toFunLike instEquivLike submoduleMap	—	RingHomSurjective.invPair
submoduleMap_symm_apply_coe 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike DFunLike.coe LinearIsometryEquiv Submodule.map RingHomSurjective.invPair ContinuousLinearMap.toLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearEquiv.toContinuousLinearMap toContinuousLinearEquiv Submodule.seminormedAddCommGroup Submodule.module EquivLike.toFunLike instEquivLike symm submoduleMap LinearEquiv.toLinearMap toLinearEquiv	—	RingHomSurjective.invPair
surjective 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike	—	LinearEquiv.surjective
symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike symm	—	LinearEquiv.symm_apply_apply
symm_bijective 📖	mathematical	—	Function.Bijective LinearIsometryEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_comp_self 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike symm	—	symm_apply_apply
symm_neg 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids neg	—	RingHomInvPair.ids
symm_prodComm 📖	mathematical	—	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.seminormedAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup prodComm	—	RingHomInvPair.ids
symm_symm 📖	mathematical	—	symm	—	—
symm_trans 📖	mathematical	—	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
toContinuousLinearEquiv_inj 📖	mathematical	—	toContinuousLinearEquiv	—	toContinuousLinearEquiv_injective
toContinuousLinearEquiv_injective 📖	mathematical	—	LinearIsometryEquiv ContinuousLinearEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup toContinuousLinearEquiv	—	coe_injective
toContinuousLinearEquiv_refl 📖	mathematical	—	toContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids refl ContinuousLinearEquiv.refl UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	RingHomInvPair.ids
toContinuousLinearEquiv_symm 📖	mathematical	—	toContinuousLinearEquiv symm ContinuousLinearEquiv.symm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—
toContinuousLinearEquiv_trans 📖	mathematical	—	toContinuousLinearEquiv trans ContinuousLinearEquiv.trans UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—
toContinuousLinearMap_toLinearIsometry 📖	mathematical	—	LinearIsometry.toContinuousLinearMap toLinearIsometry ContinuousLinearEquiv.toContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup toContinuousLinearEquiv	—	—
toHomeomorph_inj 📖	mathematical	—	toHomeomorph	—	toHomeomorph_injective
toHomeomorph_injective 📖	mathematical	—	LinearIsometryEquiv Homeomorph UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace toHomeomorph	—	coe_injective
toHomeomorph_symm 📖	mathematical	—	toHomeomorph symm Homeomorph.symm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	—
toHomeomorph_trans 📖	mathematical	—	toHomeomorph trans Homeomorph.trans UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	—
toIsometryEquiv_inj 📖	mathematical	—	toIsometryEquiv	—	toIsometryEquiv_injective
toIsometryEquiv_injective 📖	mathematical	—	LinearIsometryEquiv IsometryEquiv PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace toIsometryEquiv	—	coe_injective
toIsometryEquiv_symm 📖	mathematical	—	toIsometryEquiv symm IsometryEquiv.symm PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	—
toIsometryEquiv_trans 📖	mathematical	—	toIsometryEquiv trans IsometryEquiv.trans PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	—
toLinearEquiv_inj 📖	mathematical	—	toLinearEquiv	—	toLinearEquiv_injective
toLinearEquiv_injective 📖	mathematical	—	LinearIsometryEquiv LinearEquiv AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup toLinearEquiv	—	—
toLinearEquiv_symm 📖	mathematical	—	toLinearEquiv symm LinearEquiv.symm AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—
toLinearEquiv_trans 📖	mathematical	—	toLinearEquiv trans LinearEquiv.trans AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—
toLinearIsometry_inj 📖	mathematical	—	toLinearIsometry	—	toLinearIsometry_injective
toLinearIsometry_injective 📖	mathematical	—	LinearIsometryEquiv LinearIsometry toLinearIsometry	—	coe_injective
trans_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike instEquivLike trans	—	—
trans_assoc 📖	mathematical	—	trans	—	—
trans_one 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.right_ids RingHomCompTriple.ids LinearIsometryEquiv InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroup	—	trans_refl
trans_refl 📖	mathematical	—	trans RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.right_ids RingHomCompTriple.ids refl	—	ext RingHomInvPair.ids RingHomCompTriple.right_ids RingHomCompTriple.ids

LinearIsometryEquiv.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—
symm_apply 📖	CompOp	—

LinearMap

Definitions

Name	Category	Theorems
toLinearIsometry 📖	CompOp	—

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_linearIsometry 📖	—	DFunLike.coe LinearIsometry LinearIsometry.instFunLike Module.Basis AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instFunLike	—	—	LinearIsometry.toLinearMap_injective ext
ext_linearIsometryEquiv 📖	—	DFunLike.coe LinearIsometryEquiv EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Module.Basis AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instFunLike	—	—	LinearIsometryEquiv.toLinearEquiv_injective ext'

MulOpposite

Definitions

Name	Category	Theorems
opLinearIsometryEquiv 📖	CompOp	4 math math: toLinearEquiv_opLinearIsometryEquiv, opLinearIsometryEquiv_symm_apply, opLinearIsometryEquiv_apply, toContinuousLinearEquiv_opLinearIsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isometry_opLinearEquiv 📖	mathematical	—	Isometry MulOpposite PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace instPseudoEMetricSpace DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instAddCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv opLinearEquiv	—	RingHomInvPair.ids
opLinearIsometryEquiv_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOpposite instSeminormedAddCommGroup instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike LinearIsometryEquiv.instEquivLike opLinearIsometryEquiv op	—	RingHomInvPair.ids
opLinearIsometryEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOpposite instSeminormedAddCommGroup instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm opLinearIsometryEquiv unop	—	RingHomInvPair.ids
toContinuousLinearEquiv_opLinearIsometryEquiv 📖	mathematical	—	LinearIsometryEquiv.toContinuousLinearEquiv MulOpposite RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instSeminormedAddCommGroup instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup opLinearIsometryEquiv opContinuousLinearEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	RingHomInvPair.ids
toLinearEquiv_opLinearIsometryEquiv 📖	mathematical	—	LinearIsometryEquiv.toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOpposite instSeminormedAddCommGroup instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup opLinearIsometryEquiv opLinearEquiv	—	RingHomInvPair.ids

SemilinearIsometryClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz 📖	mathematical	—	AntilipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal instOneNNReal DFunLike.coe	—	Isometry.antilipschitz isometry
continuous 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe	—	Isometry.continuous isometry
diam_image 📖	mathematical	—	Metric.diam SeminormedAddCommGroup.toPseudoMetricSpace Set.image DFunLike.coe	—	Isometry.diam_image isometry
diam_range 📖	mathematical	—	Metric.diam SeminormedAddCommGroup.toPseudoMetricSpace Set.range DFunLike.coe Set.univ	—	Isometry.diam_range isometry
ediam_image 📖	mathematical	—	Metric.ediam PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.image DFunLike.coe	—	Isometry.ediam_image isometry
ediam_range 📖	mathematical	—	Metric.ediam PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.range DFunLike.coe Set.univ	—	Isometry.ediam_range isometry
isometry 📖	mathematical	—	Isometry PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe	—	AddMonoidHomClass.isometry_of_norm DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass toSemilinearMapClass norm_map
lipschitz 📖	mathematical	—	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NNReal instOneNNReal DFunLike.coe	—	Isometry.lipschitz isometry
nnnorm_map 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe	—	NNReal.eq norm_map
norm_map 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe	—	—
toContinuousSemilinearMapClass 📖	mathematical	—	ContinuousSemilinearMapClass UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	toSemilinearMapClass continuous
toSemilinearMapClass 📖	mathematical	—	SemilinearMapClass AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—

SemilinearIsometryEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_map 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe EquivLike.toFunLike	—	—
toSemilinearEquivClass 📖	mathematical	—	SemilinearEquivClass AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	—
toSemilinearIsometryClass 📖	mathematical	—	SemilinearIsometryClass EquivLike.toFunLike	—	AddEquivClass.map_add SemilinearEquivClass.toAddEquivClass toSemilinearEquivClass SemilinearEquivClass.map_smulₛₗ norm_map

Submodule

Definitions

Name	Category	Theorems
subtypeₗᵢ 📖	CompOp	12 math math: OrthogonalFamily.of_pairwise, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, subtypeₗᵢ_toContinuousLinearMap, subtypeₗᵢ_toLinearMap, orthogonalFamily_self, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, coe_subtypeₗᵢ, AffineSubspace.subtypeₐᵢ_linearIsometry, orthogonalFamily_iff_pairwise, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces, isHilbertSumOrthogonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_subtypeₗᵢ 📖	mathematical	—	DFunLike.coe LinearIsometry Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership setLike seminormedAddCommGroup module LinearIsometry.instFunLike subtypeₗᵢ LinearMap addCommMonoid LinearMap.instFunLike subtype	—	—
subtypeₗᵢ_toContinuousLinearMap 📖	mathematical	—	LinearIsometry.toContinuousLinearMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership setLike RingHom.id Semiring.toNonAssocSemiring seminormedAddCommGroup module subtypeₗᵢ subtypeL UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	—
subtypeₗᵢ_toLinearMap 📖	mathematical	—	LinearIsometry.toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SetLike.instMembership setLike seminormedAddCommGroup module subtypeₗᵢ subtype	—	—

(root)

Definitions

Name	Category	Theorems
LinearIsometry 📖	CompData	119 math math: TensorProduct.mapInclIsometry_apply, LinearIsometry.coe_toLinearMap, IsHilbertSum.surjective_isometry, OrthogonalFamily.linearIsometry_apply_single, LinearIsometry.lipschitz, LinearIsometry.diam_image, RCLike.ofRealLI_apply, LinearIsometry.map_smul, Complex.ofRealLI_apply, LinearIsometry.isComplete_image_iff', LinearIsometry.one_def, LinearIsometry.coe_toLinearIsometryEquiv, LinearIsometry.norm_map, IsHilbertSum.linearIsometryEquiv_symm_apply, OrthogonalFamily.orthonormal_sigma_orthonormal, LinearIsometry.map_add, LinearIsometry.isEmbedding, LinearIsometry.map_starProjection', LinearIsometry.coe_toContinuousLinearMap, OrthogonalFamily.norm_sq_diff_sum, IsHilbertSum.hasSum_linearIsometryEquiv_symm, LinearIsometry.preimage_closedBall, LinearIsometry.coe_one, InnerProductSpace.toDualMap_apply_apply, LinearIsometry.ext_iff, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, LinearIsometry.enorm_map, LinearIsometry.map_sub, LinearIsometry.edist_map, LinearIsometry.id_apply, LinearIsometry.mul_def, LinearIsometry.equivRange_apply_coe, LinearIsometry.inner_map_map, LinearIsometry.lTensor_apply, MeasureTheory.Lp.compMeasurePreservingₗᵢ_apply_coe, InnerProductSpace.toDualMap_apply, LinearIsometry.extend_apply, ContinuousAlternatingMap.toContinuousMultilinearMapLI_apply, Submodule.IsOrtho.map, LinearIsometryEquiv.coe_ofLinearIsometry, LinearIsometry.ediam_image, LinearIsometry.coe_pow, LinearIsometry.dist_map, LinearIsometry.norm_iteratedFDeriv_comp_left, Submodule.HasOrthogonalProjection.map_linearIsometryEquiv', LinearIsometry.toSpanSingleton_apply, OrthogonalFamily.hasSum_linearIsometry, LinearIsometry.continuous, AffineIsometry.map_vsub, LinearIsometryEquiv.toLinearIsometry_injective, OrthogonalFamily.summable_of_lp, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, LinearIsometry.preimage_ball, ContinuousLinearMap.coe_restrictScalarsIsometry, LinearIsometry.injective, LinearIsometry.map_neg, LinearIsometry.map_smulₛₗ, LinearIsometry.toLinearMap_injective, LinearIsometry.norm_iteratedFDerivWithin_comp_left, Submodule.coe_subtypeₗᵢ, LinearIsometry.inr_apply, LinearIsometry.orthonormal_comp_iff, LinearIsometryEquiv.coe_toLinearIsometry, OrthogonalFamily.inner_sum, LinearIsometry.coe_injective, LinearIsometry.map_starProjection, LinearIsometry.coe_id, LinearIsometry.preimage_sphere, LinearIsometry.coe_toAffineIsometry, LinearIsometry.comp_continuous_iff, ContinuousAlternatingMap.restrictScalarsLI_apply, UniformSpace.Completion.coe_toComplₗᵢ, LinearIsometry.isometry, LinearIsometry.integral_comp_comm, StrictConvex.linearIsometry_preimage, LinearIsometry.antilipschitz, OrthogonalFamily.eq_ite, LinearIsometry.coe_comp, LinearIsometry.diam_range, LinearMap.coe_isometryOfInner, InnerProductSpace.toDual_apply_eq_toDualMap_apply, LinearIsometry.map_eq_iff, AffineIsometry.map_vadd, MeasureTheory.charFun_eq_charFunDual_toDualMap, LinearIsometry.completeSpace_map, MeasureTheory.withDensitySMulLI_apply, LinearMap.coe_isometryOfOrthonormal, TensorProduct.mapIsometry_apply, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, LinearIsometry.contDiff, LinearIsometry.toContinuousLinearMap_injective, LinearIsometry.strictConvexSpace_range_iff, LinearIsometry.coe_mul, LinearIsometry.inl_apply, LinearIsometry.ediam_range, ContinuousAlternatingMap.curryLeftLI_apply, OrthogonalFamily.norm_sum, LinearIsometry.strictConvexSpace_range, LinearIsometry.map_zero, IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.nnnorm_map, LinearIsometry.withLpProdMap_apply, LinearIsometry.coe_mk, LinearIsometry.toLinearIsometryEquiv_apply, LinearIsometry.rTensor_apply, EuclideanGeometry.Sphere.secondInter_map, OrthogonalFamily.linearIsometry_apply, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, OrthogonalFamily.summable_iff_norm_sq_summable, Orientation.rotationAux_apply, LinearIsometry.instSemilinearIsometryClass, Submodule.IsOrtho.comap, LinearIsometry.submoduleMap_apply_coe, OrthogonalFamily.inner_right_fintype, LinearIsometry.angle_map, ContinuousLinearMap.coe_mulₗᵢ, OrthogonalFamily.inner_right_dfinsupp, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, Orthonormal.comp_linearIsometry
LinearIsometryClass 📖	MathDef	—
LinearIsometryEquiv 📖	CompData	519 math math: OrthonormalBasis.singleton_repr, LinearMap.IsSymmetric.clm_adjoint_eq, DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, LinearIsometryEquiv.strictConvex_preimage, fderiv_iteratedFDeriv, Orientation.kahler_map_complex, LinearIsometryEquiv.hasStrictFDerivAt, LinearIsometryEquiv.comp_fderiv, LinearIsometryEquiv.coe_symm_toIsometryEquiv, LinearIsometryEquiv.surjective, LinearIsometryEquiv.analyticOnNhd, hasFDerivAt_iff_hasGradientAt, LinearIsometryEquiv.coe_ofLinearIsometry_symm, LinearIsometryEquiv.trans_one, Orientation.inner_rotation_pi_div_two_right_smul, Orientation.oangle_add_left_smul_rotation_pi_div_two, Real.fourierIntegral_comp_linearIsometry, Submodule.orthogonalDecomposition_symm_apply, IsometryEquiv.toRealLinearIsometryEquiv_symm_apply, OrthonormalBasis.repr_injective, LinearIsometryEquiv.symm_bijective, hasFTaylorSeriesUpToOn_top_iff_right, Orientation.tan_oangle_add_left_smul_rotation_pi_div_two, LinearIsometry.coe_toLinearIsometryEquiv, Orientation.rotation_eq_self_iff, Submodule.reflection_orthogonal_apply, LinearMap.IsSymmetric.diagonalization_apply_self_apply, LinearIsometryEquiv.comp_fderivWithin, LinearIsometryEquiv.antilipschitz, ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries, iteratedFDerivWithin_succ_eq_comp_right, LinearIsometryEquiv.fderivWithin, HasFTaylorSeriesUpTo.hasFDerivAt, Orientation.neg_rotation, Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, LinearMap.adjoint_eq_toCLM_adjoint, Orientation.eq_rotation_self_iff_angle_eq_zero, IsometryEquiv.toRealLinearIsometryEquiv_apply, LinearIsometryEquiv.range_eq_univ, rotation_injective, InnerProductSpace.toDual_symm_apply, IsHilbertSum.linearIsometryEquiv_symm_apply, Orientation.tan_oangle_add_right_smul_rotation_pi_div_two, LinearIsometryEquiv.ext_iff, Complex.conjLIE_apply, LinearIsometryEquiv.coe_symm_toHomeomorph, MeasureTheory.charFun_toDual_symm_eq_charFunDual, LinearIsometryEquiv.coe_mk, ContinuousAlternatingMap.piLIE_apply_apply, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, ContinuousLinearMap.adjoint_id, iteratedFDerivWithin_succ_eq_comp_left, ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, LinearIsometryEquiv.norm_map, LinearIsometryEquiv.map_zero, LinearIsometryEquiv.apply_symm_apply, LinearIsometryEquiv.coe_toAffineIsometryEquiv, OrthonormalBasis.repr_self, ContinuousLinearMap.eq_adjoint_iff, Orientation.volumeForm_map, rotation_apply, toMatrix_rotation, LinearIsometryEquiv.piLpCongrRight_apply, Unitary.coe_linearIsometryEquiv_apply, Submodule.reflection_singleton_apply, HasFTaylorSeriesUpToOn.zero_eq', Orientation.inner_rightAngleRotation_swap', IsSelfAdjoint.adjoint_eq, OrthonormalBasis.measurePreserving_repr, Submodule.reflection_apply, LinearIsometryEquiv.lTensor_apply, EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint, ContinuousLinearMap.isPositive_self_comp_adjoint, LinearMap.adjoint_toContinuousLinearMap, LinearIsometryEquiv.coe_neg, Unitary.linearIsometryEquiv_coe_apply, LinearIsometryEquiv.image_eq_preimage_symm, LinearIsometryEquiv.adjoint_eq_symm, Orientation.neg_rotation_neg_pi_div_two, LinearIsometryEquiv.trans_smul, IsHilbertSum.hasSum_linearIsometryEquiv_symm, ContinuousAlternatingMap.constOfIsEmptyLIE_apply, LinearEquiv.coe_isometryOfOrthonormal, LinearIsometryEquiv.inner_map_eq_flip, Quaternion.linearIsometryEquivTuple_symm_apply, ContinuousAlternatingMap.ofSubsingletonLIE_symm_apply, LinearIsometryEquiv.fderiv, LinearIsometryEquiv.measurePreserving, LinearIsometryEquiv.coe_toLinearEquiv, Orientation.rotation_pi_apply, Orientation.rotation_rotation, LinearIsometryEquiv.coe_toHomeomorph, Orientation.rotation_map_complex, TensorProduct.lidIsometry_apply, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, Module.Basis.coe_toOrthonormalBasis_repr, LinearIsometryEquiv.map_add, AffineIsometryEquiv.map_vsub, Orientation.kahler_comp_rightAngleRotation, LinearIsometryEquiv.coe_ofEq_apply, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, hasGradientWithinAt_iff_hasFDerivWithinAt, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left, LinearIsometryEquiv.smul_apply, LinearIsometryEquiv.toIsometryEquiv_injective, LinearIsometryEquiv.coe_injective, LinearIsometryEquiv.contDiff, ContinuousMultilinearMap.curryFinFinset_symm_apply_const, HasFPowerSeriesOnBall.fderiv_eq, LinearIsometryEquiv.coe_trans, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff', LinearIsometryEquiv.piLpCongrLeft_apply, unitary.linearIsometryEquiv_coe_symm_apply, HasFTaylorSeriesUpToOn.hasFDerivWithinAt, OrthonormalBasis.coe_ofRepr, Submodule.adjoint_subtypeL, LinearIsometry.equivRange_apply_coe, RCLike.conjLIE_apply, Submodule.reflection_orthogonalComplement_singleton_eq_neg, LinearIsometryEquiv.reflections_generate_dim_aux, Complex.orthonormalBasisOneI_repr_apply, LinearIsometryEquiv.coe_toContinuousLinearEquiv, Real.fourierIntegralInv_comp_linearIsometry, Orientation.rotation_map, Orientation.oangle_rotation_left, EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, HasFPowerSeriesWithinAt.fderivWithin_eq, ContinuousLinearMap.IsPositive.conj_adjoint, Unitary.coe_symm_linearIsometryEquiv_apply, LinearIsometryEquiv.diam_image, InnerProductSpace.adjoint_rankOne, LinearIsometryEquiv.ofTop_symm_apply_coe, HilbertBasis.hasSum_repr, HasFDerivWithinAt.hasGradientWithinAt, Real.fourier_comp_linearIsometry, LinearMap.IsSymmetric.diagonalization_symm_apply, PiTensorProduct.liftIsometry_tprodL, LinearIsometryEquiv.coe_toMeasurableEquiv, LinearIsometryEquiv.image_sphere, LinearIsometryEquiv.nnnorm_map, InnerProductSpace.toDual_apply, OrthonormalBasis.tensorProduct_repr_tmul_apply', Real.fourierInv_comp_linearIsometry, LinearIsometryEquiv.reflections_generate, iteratedFDerivWithin_eq_equiv_comp, MeasureTheory.integrable_comp, LinearIsometryEquiv.map_eq_iff, ContinuousLinearMap.adjoint_inner_left, Orientation.oangle_rotation_oangle_right, LinearIsometryEquiv.coe_prodAssoc_symm, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right, ContinuousMultilinearMap.ofSubsingletonₗᵢ_symm_apply, LinearIsometryEquiv.preimage_ball, continuousMultilinearCurryFin0_symm_apply, ContinuousAlternatingMap.ofSubsingletonLIE_apply, continuousMultilinearCurryRightEquiv_symm_apply, OrthonormalBasis.equiv_apply, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, ContinuousMap.linearIsometryBoundedOfCompact_symm_apply, LinearIsometryEquiv.congr_arg, Module.Basis.coe_toOrthonormalBasis_repr_symm, InnerProductSpace.toDual_apply_apply, ContinuousLinearMap.adjointAux_apply, Orientation.inner_rotation_pi_div_two_right, coe_lpBCFₗᵢ, ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self, LinearIsometryEquiv.comp_differentiableOn_iff, LinearIsometryEquiv.comp_differentiableAt_iff, Orientation.oangle_rotation, ContinuousLinearMap.coe_flipₗᵢ', LinearIsometryEquiv.conjStarAlgEquiv_ext_iff, OrthonormalBasis.repr_apply_apply, ContinuousAlternatingMap.constOfIsEmptyLIE_symm_apply, Orientation.inner_rotation_pi_div_two_left, LinearEquiv.extendOfIsometry_symm_eq, ContinuousMap.toLp_def, ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker, Orientation.oangle_rotation_self_left, ContinuousMultilinearMap.prodL_apply, hasFTaylorSeriesUpToOn_succ_iff_right, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, LinearIsometryEquiv.coe_toIsometryEquiv, LinearIsometryEquiv.piLpCurry_apply, Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero, LinearIsometryEquiv.coe_ofLinearIsometry, LinearMap.toMatrix_innerₛₗ_apply, ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff, Orientation.inner_rotation_pi_div_two_left_smul, LinearEquiv.extendOfIsometry_symm_apply, LinearIsometryEquiv.toLinearEquiv_injective, LinearIsometryEquiv.image_ball, Submodule.reflection_mem_subspace_orthogonal_precomplement_eq_neg, LinearIsometryEquiv.toHomeomorph_injective, fderivWithin_iteratedFDerivWithin, Orientation.eq_rotation_self_iff, LinearIsometryEquiv.piLpCongrRight_single, Submodule.fst_orthogonalDecomposition_apply, LinearIsometryEquiv.dist_map, Orientation.inner_comp_rightAngleRotation, LinearIsometryEquiv.continuousWithinAt, ContinuousMultilinearMap.curryFinFinset_apply_const, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left, inner_map_complex, HasGradientAt.hasFDerivAt, Submodule.reflection_reflection, hasFTaylorSeriesUpTo_succ_nat_iff_right, LinearIsometryEquiv.coe_symm_toLinearEquiv, Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero, EuclideanGeometry.reflection_apply_of_mem, Orthonormal.linearIsometryEquiv_symm_apply_single_one, iteratedFDeriv_eq_equiv_comp, Submodule.reflection_inv, linear_isometry_complex, hasFTaylorSeriesUpToOn_succ_nat_iff_right, LinearIsometryEquiv.toLinearIsometry_injective, Unitary.linearIsometryEquiv_coe_symm_apply, Orientation.oangle_rotation_oangle_left, ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense, LinearIsometryEquiv.analyticWithinAt, LinearIsometryEquiv.toSpanUnitSingleton_apply, Submodule.reflection_mul_reflection, rotationOf_rotation, Submodule.starProjection_map_apply, LinearIsometryEquiv.coe_coe, HasFPowerSeriesAt.fderiv_eq, continuousMultilinearCurryFin0_apply, EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, Orientation.rightAngleRotation_rightAngleRotation, IsSelfAdjoint.conj_adjoint, ContinuousMultilinearMap.curryMidEquiv_apply, Orientation.areaForm_comp_linearIsometryEquiv, LinearIsometryEquiv.ofTop_apply, LinearIsometryEquiv.comp_differentiableWithinAt_iff, LinearIsometryEquiv.withLpProdCongr_symm_apply, Submodule.reflection_sub, LinearEquiv.extendOfIsometry_apply, Orientation.rotation_eq_self_iff_angle_eq_zero, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, LinearEquiv.coe_isometryOfInner, Orientation.oangle_rotation_right, starₗᵢ_apply, LinearIsometryEquiv.toLinearEquiv_smul, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, LinearIsometryEquiv.analyticOn, LinearIsometryEquiv.analyticAt, EuclideanSpace.basisFun_repr, HasFTaylorSeriesUpToOn.hasFDerivAt, RCLike.realLinearIsometryEquiv_symm_apply, Orientation.oangle_sub_right_smul_rotation_pi_div_two, ContinuousLinearMap.isSelfAdjoint_iff', OrthonormalBasis.equiv_apply_euclideanSpace, Complex.orthonormalBasisOneI_repr_symm_apply, LinearIsometryEquiv.symm_comp_self, iteratedDeriv_eq_equiv_comp, HasFTaylorSeriesUpToOn.shift_of_succ, Orientation.areaForm_comp_rightAngleRotation, LinearIsometryEquiv.contDiffPointwiseHolderAt_left_comp, MeasureTheory.integral_comp, RCLike.complexLinearIsometryEquiv_symm_apply, coe_lpPiLpₗᵢ, LinearIsometryEquiv.coe_coe'', Orientation.inner_rightAngleRotation_left, LinearIsometryEquiv.coe_toLinearIsometry, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left, LinearIsometryEquiv.coe_withLpProdUnique, OrthonormalBasis.map_apply, LinearIsometryEquiv.trans_apply, OrthonormalBasis.sum_repr_symm, Orientation.inner_smul_rotation_pi_div_two_right, IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero, LinearIsometryEquiv.strictConvex_image, Orientation.kahler_rotation_left', rotation_trans, ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const, LinearIsometryEquiv.edist_map, hasGradientAt_iff_hasFDerivAt, FormalMultilinearSeries.leftInv_coeff_one, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, TensorProduct.assocIsometry_apply, LinearIsometryEquiv.injective, MulOpposite.opLinearIsometryEquiv_symm_apply, LinearIsometryEquiv.hasFDerivAt, LinearIsometryEquiv.rTensor_apply, LinearIsometryEquiv.inner_map_map, Orientation.neg_rotation_pi_div_two, ContinuousAlternatingMap.piLIE_symm_apply_apply, HasFPowerSeriesAt.hasFDerivAt, OrthonormalBasis.measurePreserving_repr_symm, Orientation.linearIsometryEquiv_comp_rightAngleRotation, EuclideanSpace.piLpCongrLeft_single, LinearIsometryEquiv.norm_iteratedFDeriv_comp_right, Orientation.inner_rightAngleRotation_swap, LinearIsometryEquiv.piLpCurry_symm_apply, rotationOf_coe, LinearIsometryEquiv.coe_inv, Orientation.oangle_sub_left_smul_rotation_pi_div_two, Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero, LinearIsometryEquiv.map_sub, LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply, Orientation.oangle_add_right_smul_rotation_pi_div_two, LinearIsometryEquiv.symm_apply_apply, Orientation.inner_smul_rotation_pi_div_two_left, LinearIsometryEquiv.isometry, LinearIsometryEquiv.submoduleMap_symm_apply_coe, InnerProductSpace.rankOne_comp, Orientation.kahler_rightAngleRotation_left, Orientation.kahler_comp_linearIsometryEquiv, InnerProductSpace.toMatrix_rankOne, PiTensorProduct.liftIsometry_comp_mapL, continuousMultilinearCurryLeftEquiv_apply, WStarAlgebra.exists_predual, Orientation.kahler_rotation_left, PiTensorProduct.liftIsometry_symm_apply, iteratedFDeriv_succ_eq_comp_right, ContinuousLinearMap.adjoint_toSpanSingleton, LinearIsometryEquiv.coe_one, coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, LinearIsometryEquiv.coe_ofSurjective, Submodule.reflection_eq_self_iff, HasFPowerSeriesWithinOnBall.fderivWithin_eq, ContinuousMultilinearMap.piₗᵢ_symm_apply, linearEquiv_det_rotation, HasFTaylorSeriesUpToOn.hasStrictFDerivAt, LinearIsometryEquiv.prodComm_symm_apply, LinearIsometryEquiv.coe_symm_toContinuousLinearEquiv, OrthonormalBasis.repr_symm_single, Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two, LinearIsometryEquiv.withLpProdCongr_apply, coe_starₗᵢ, InnerProductSpace.toDual_apply_eq_toDualMap_apply, Orientation.oangle_map, Submodule.reflection_map_apply, LinearIsometryEquiv.continuousAt, HasFPowerSeriesOnBall.hasFDerivAt, LinearIsometryEquiv.withLpProdUnique_symm_apply, toMatrix_innerSL_apply, OrthonormalBasis.equiv_apply_basis, LinearIsometryEquiv.self_comp_symm, ContinuousLinearMap.orthogonal_range, Orientation.kahler_map, LinearIsometryEquiv.comp_differentiable_iff, LinearIsometryEquiv.coe_refl, PiTensorProduct.liftIsometry_apply_apply, ContinuousMultilinearMap.prodL_symm_apply, ProbabilityTheory.covarianceBilin_map, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, Orientation.coe_basisRightAngleRotation, LinearIsometryEquiv.smul_trans, LinearIsometryEquiv.continuousOn, Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero, Orientation.areaForm_map, ContinuousMap.linearIsometryBoundedOfCompact_apply_apply, LinearIsometryEquiv.congr_fun, ContinuousLinearMap.adjoint_comp, iteratedFDeriv_zero_eq_comp, LinearIsometryEquiv.map_eq_zero_iff, HilbertBasis.repr_self, TensorProduct.commIsometry_apply, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', continuousMultilinearCurryRightEquiv_symm_apply', iteratedDerivWithin_eq_equiv_comp, Submodule.adjoint_orthogonalProjection, LinearIsometryEquiv.mul_refl, hasFDerivWithinAt_iff_hasGradientWithinAt, ContinuousAlternatingMap.prodLIE_apply, LinearIsometryEquiv.comp_hasFDerivAt_iff', PadicInt.mahlerEquiv_apply, Submodule.reflection_involutive, LinearIsometryEquiv.comp_continuousOn_iff, ContinuousLinearMap.IsPositive.adjoint_conj, LinearIsometryEquiv.reflections_generate_dim, Complex.isometryOfOrthonormal_apply, LinearIsometryEquiv.withLpProdUnique_apply, Orientation.areaForm_map_complex, MulOpposite.opLinearIsometryEquiv_apply, LinearIsometryEquiv.comp_hasFDerivAt_iff, ContinuousLinearMap.star_eq_adjoint, Orientation.inner_rightAngleRotation_right, ProperCone.hyperplane_separation_of_notMem, iteratedFDerivWithin_zero_eq_comp, Orientation.rotation_apply, ContinuousLinearMap.coe_flipₗᵢ, OrthonormalBasis.sum_repr, Submodule.reflection_mem_subspace_eq_self, IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero_symm, LinearIsometryEquiv.hasFDerivWithinAt, LinearIsometryEquiv.symm_units_smul, IsHilbertSum.linearIsometryEquiv_symm_apply_single, IsSelfAdjoint.adjoint_conj, AffineIsometryEquiv.map_vadd, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr, LinearIsometryEquiv.lipschitz, LinearIsometryEquiv.piLpCongrLeft_single, ContinuousLinearMap.adjoint_inner_right, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, LinearIsometryEquiv.symm_smul_apply, OrthonormalBasis.coe_toBasis_repr_apply, det_rotation, LinearIsometryEquiv.toContinuousLinearEquiv_injective, LinearIsometryEquiv.coe_symm_trans, OrthonormalBasis.coe_equiv_euclideanSpace, Orientation.rightAngleRotation_map, Orientation.kahler_rotation_right, continuousMultilinearCurryRightEquiv_apply', Orthonormal.comp_linearIsometryEquiv, HasFiniteFPowerSeriesOnBall.hasFDerivAt, HasFDerivAt.hasGradientAt, rotation_symm, ContinuousLinearMap.isAdjointPair_inner, LinearIsometryEquiv.differentiableAt, LinearIsometryEquiv.differentiable, Submodule.snd_orthogonalDecomposition_apply, LinearIsometryEquiv.withLpProdComm_apply, LinearEquiv.extendOfIsometry_eq, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, Orientation.oangle_rotation_self_right, LinearIsometryEquiv.withLpProdAssoc_apply, continuousMultilinearCurryLeftEquiv_symm_apply, Submodule.orthogonalDecomposition_apply, iteratedFDeriv_succ_eq_comp_left, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff, LinearIsometryEquiv.one_def, LinearIsometryEquiv.prodComm_apply, ContinuousMultilinearMap.piₗᵢ_apply, Orientation.areaForm_rightAngleRotation_right, ContinuousMultilinearMap.ofSubsingletonₗᵢ_apply, LinearIsometry.toLinearIsometryEquiv_apply, continuousMultilinearCurryFin1_symm_apply, LinearIsometryEquiv.instSemilinearIsometryEquivClass, PadicInt.mahlerEquiv_symm_apply, Orientation.inner_smul_rotation_pi_div_two_smul_left, LinearIsometryEquiv.mul_def, LinearIsometryEquiv.comp_continuous_iff, Orientation.oangle_map_complex, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, LinearIsometryEquiv.map_smul, ContinuousLinearMap.norm_adjoint_comp_self, Orientation.inner_smul_rotation_pi_div_two_smul_right, Complex.rightAngleRotation, HasFTaylorSeriesUpTo.zero_eq', ContinuousMultilinearMap.curryFinFinset_symm_apply, Orientation.kahler_rightAngleRotation_right, Quaternion.linearIsometryEquivTuple_apply, ContinuousAffineMap.toConstProdContinuousLinearMap_fst, LinearIsometryEquiv.integrable_comp_iff, Complex.isometryOfOrthonormal_symm_apply, LinearIsometryEquiv.inv_def, Orientation.inner_rightAngleRotation_self, HasFiniteFPowerSeriesOnBall.fderiv_eq, LinearIsometryEquiv.continuous, TensorProduct.congrIsometry_apply, HasFPowerSeriesAt.hasStrictFDerivAt, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right, ContinuousLinearMap.isPositive_adjoint_comp_self, LinearIsometryEquiv.refl_mul, continuousMultilinearCurryRightEquiv_apply, ContinuousAlternatingMap.prodLIE_symm_apply, HasFPowerSeriesWithinAt.hasFDerivWithinAt, LinearIsometryEquiv.norm_iteratedFDeriv_comp_left, Orientation.rotation_symm_apply, LinearIsometryEquiv.withLpUniqueProd_apply, LinearIsometryEquiv.coe_mul, HasGradientWithinAt.hasFDerivWithinAt, FormalMultilinearSeries.rightInv_coeff_one, Orientation.volumeForm_comp_linearIsometryEquiv, Pi.orthonormalBasis_repr, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, Orientation.rotation_oangle_eq_iff_norm_eq, ContinuousLinearMap.fpowerSeries_apply_one, LinearIsometryEquiv.toContinuousLinearEquiv_smul, ContinuousMultilinearMap.curryFinFinset_apply, LinearIsometryEquiv.differentiableOn, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, Orthonormal.equiv_apply, Orientation.rightAngleRotation_neg_orientation, Orientation.rotationAux_apply, LinearIsometryEquiv.withLpUniqueProd_symm_apply, HasFPowerSeriesWithinOnBall.hasFDerivWithinAt, OrthonormalBasis.repr_reindex, LinearIsometryEquiv.differentiableWithinAt, ContinuousLinearMap.adjoint_innerSL_apply, EuclideanGeometry.reflection_apply, LinearIsometryEquiv.comp_fderiv', RCLike.realLinearIsometryEquiv_apply, Orientation.rightAngleRotation_map_complex, Orientation.areaForm_rightAngleRotation_left, ContinuousLinearMap.fpowerSeriesBilinear_apply_one, OrthonormalBasis.tensorProduct_repr_tmul_apply, TensorProduct.assocIsometry_symm_apply, Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg, PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp, ContinuousLinearMap.innerSL_apply_comp, TensorProduct.lidIsometry_symm_apply, HilbertBasis.hasSum_repr_symm, LinearIsometryEquiv.comp_hasStrictFDerivAt_iff, LinearIsometryEquiv.one_trans, LinearIsometryEquiv.withLpProdAssoc_symm_apply, ContinuousLinearMap.adjoint_adjoint, LinearIsometryEquiv.coe_prodAssoc, LinearIsometryEquiv.preimage_sphere, LinearIsometryEquiv.coe_withLpUniqueProd, LinearIsometryEquiv.image_closedBall, ContinuousLinearMap.orthogonal_ker, Complex.rotation, RCLike.complexLinearIsometryEquiv_apply, LinearIsometryEquiv.map_smulₛₗ, ContinuousAffineMap.toConstProdContinuousLinearMap_snd, ContinuousMultilinearMap.curryMidEquiv_symm_apply, LinearIsometryEquiv.ediam_image, LinearIsometryEquiv.bijective, LinearIsometryEquiv.submoduleMap_apply_coe, LinearIsometryEquiv.coe_symm_toMeasurableEquiv, LinearIsometryEquiv.preimage_closedBall, continuousMultilinearCurryFin1_apply, unitary.linearIsometryEquiv_coe_apply
LinearIsometryEquivClass 📖	MathDef	—
SemilinearIsometryClass 📖	CompData	2 math math: SemilinearIsometryEquivClass.toSemilinearIsometryClass, LinearIsometry.instSemilinearIsometryClass
SemilinearIsometryEquivClass 📖	CompData	1 math math: LinearIsometryEquiv.instSemilinearIsometryEquivClass
«term_→ₗᵢ[_]_» 📖	CompOp	—
«term_→ₗᵢ⋆[_]_» 📖	CompOp	—
«term_→ₛₗᵢ[_]_» 📖	CompOp	—
«term_≃ₗᵢ[_]_» 📖	CompOp	—
«term_≃ₗᵢ⋆[_]_» 📖	CompOp	—
«term_≃ₛₗᵢ[_]_» 📖	CompOp	—

---

← Back to Index