ConformalLinearMap

Statistics

Metric	Count
Definitions	0
Theorems `isConformalMap_iff`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`isConformalMap_iff` 📖	mathematical	—	`IsConformalMap` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `Real.instLT` `Real.instZero` `Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `Real.instMul`	—	`mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `real_inner_smul_right` `real_inner_smul_left` `LinearIsometry.inner_map_map` `mul_assoc` `Real.sqrt_pos` `Real.mul_self_sqrt` `LT.lt.le` `LT.lt.ne'` `smulCommClass_self` `inv_mul_cancel_left₀` `ContinuousLinearMap.ext` `smul_inv_smul₀`

---