Documentation Verification Report

IsometryEquiv

📁 Source: Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

Statistics

Metric	Count
Definitions `IsometryEquiv`, `isometryEquivWeightedSumSquares`, `isometryEquivWeightedSumSquaresWeightedSumSquares`, `weightedSumSquaresCongr`, `Equivalent`, `IsometryEquiv`, `instCoeOutLinearEquivId`, `instEquivLike`, `refl`, `toIsometry`, `toLinearEquiv`, `trans`, `isometryEquivBasisRepr`, `isometryEquivOfCompLinearEquiv`	14
Theorems `equivalent_weightedSumSquares`, `equivalent_weightedSumSquares_units_of_nondegenerate'`, `refl`, `trans`, `apply_symm_apply`, `coe_symm_toLinearEquiv`, `coe_toLinearEquiv`, `instLinearEquivClass`, `map_app`, `map_app'`, `symm_apply_apply`, `toIsometry_apply`	12
Total	26

QuadraticForm

Definitions

Name	Category	Theorems
`isometryEquivWeightedSumSquares` 📖	CompOp	—
`isometryEquivWeightedSumSquaresWeightedSumSquares` 📖	CompOp	—
`weightedSumSquaresCongr` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivalent_weightedSumSquares` 📖	mathematical	—	`QuadraticMap.Equivalent` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Pi.addCommMonoid` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.Function.module` `Semiring.toModule` `QuadraticMap.weightedSumSquares` `Fin.fintype` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.to_smulCommClass` `Algebra.id`	—	`Nat.instAtLeastTwoHAddOfNat` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `Algebra.to_smulCommClass` `LinearMap.BilinForm.exists_orthogonal_basis` `associated_isSymm`
`equivalent_weightedSumSquares_units_of_nondegenerate'` 📖	mathematical	`LinearMap.SeparatingLeft` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Semiring.toModule` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `LinearMap` `QuadraticMap` `LinearMap.BilinMap` `QuadraticMap.instAddCommMonoid` `LinearMap.addCommMonoid` `LinearMap.module` `QuadraticMap.instModuleOfSMulCommClass` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `LinearMap.instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.instFunLike` `QuadraticMap.associated` `QuadraticMap.instInvertibleEndOfNat`	`QuadraticMap.Equivalent` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Pi.addCommMonoid` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.Function.module` `Semiring.toModule` `QuadraticMap.weightedSumSquares` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fin.fintype` `Units.instMonoid` `Units.instDistribMulAction` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Units.smulCommClass_left` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.toSMul` `Algebra.id` `Algebra.to_smulCommClass`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `LinearMap.instSMulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `Units.smulCommClass_left` `Algebra.to_smulCommClass` `LinearMap.BilinForm.exists_orthogonal_basis` `associated_isSymm` `LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft` `EuclideanDomain.toNontrivial` `QuadraticMap.associated_eq_self_apply`

QuadraticMap

Definitions

Name	Category	Theorems
`Equivalent` 📖	MathDef	15 math math: `QuadraticForm.equivalent_signType_weighted_sum_squared`, `QuadraticForm.equivalent_one_neg_one_weighted_sum_squared`, `Equivalent.trans`, `QuadraticForm.equivalent_of_isAlgClosed`, `QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed`, `QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared`, `QuadraticForm.equivalent_weightedSumSquares`, `Equivalent.symm`, `QuadraticForm.equivalent_sum_squares`, `Equivalent.prod`, `QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared`, `Equivalent.refl`, `Equivalent.pi`, `QuadraticForm.complex_equivalent`, `QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'`
`IsometryEquiv` 📖	CompData	18 math math: `CategoryTheory.Iso.toIsometryEquiv_toFun`, `IsometryEquiv.toIsometry_apply`, `QuadraticForm.tensorRId_symm_apply`, `QuadraticForm.tensorRId_apply`, `IsometryEquiv.instLinearEquivClass`, `IsometryEquiv.map_app`, `QuadraticForm.tensorLId_symm_apply`, `QuadraticForm.tensorComm_apply`, `QuadraticForm.dualProdIsometry_toFun`, `QuadraticForm.tensorAssoc_symm_apply`, `QuadraticForm.tensorLId_apply`, `IsometryEquiv.prodComm_toFun`, `IsometryEquiv.coe_toLinearEquiv`, `QuadraticForm.dualProdProdIsometry_toFun`, `QuadraticForm.tensorAssoc_apply`, `IsometryEquiv.prodProdProdComm_toFun`, `IsometryEquiv.apply_symm_apply`, `IsometryEquiv.symm_apply_apply`
`isometryEquivBasisRepr` 📖	CompOp	—
`isometryEquivOfCompLinearEquiv` 📖	CompOp	—

QuadraticMap.Equivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`QuadraticMap.Equivalent`	—	—
`trans` 📖	mathematical	—	`QuadraticMap.Equivalent`	—	—

QuadraticMap.IsometryEquiv

Definitions

Name	Category	Theorems
`instCoeOutLinearEquivId` 📖	CompOp	—
`instEquivLike` 📖	CompOp	18 math math: `CategoryTheory.Iso.toIsometryEquiv_toFun`, `toIsometry_apply`, `QuadraticForm.tensorRId_symm_apply`, `QuadraticForm.tensorRId_apply`, `instLinearEquivClass`, `map_app`, `QuadraticForm.tensorLId_symm_apply`, `QuadraticForm.tensorComm_apply`, `QuadraticForm.dualProdIsometry_toFun`, `QuadraticForm.tensorAssoc_symm_apply`, `QuadraticForm.tensorLId_apply`, `prodComm_toFun`, `coe_toLinearEquiv`, `QuadraticForm.dualProdProdIsometry_toFun`, `QuadraticForm.tensorAssoc_apply`, `prodProdProdComm_toFun`, `apply_symm_apply`, `symm_apply_apply`
`refl` 📖	CompOp	3 math math: `CliffordAlgebra.equivOfIsometry_refl`, `CategoryTheory.Iso.toIsometryEquiv_refl`, `QuadraticModuleCat.ofIso_refl`
`toIsometry` 📖	CompOp	10 math math: `QuadraticModuleCat.ofIso_hom`, `toIsometry_apply`, `QuadraticModuleCat.toIsometry_hom_leftUnitor`, `QuadraticModuleCat.toIsometry_hom_rightUnitor`, `QuadraticModuleCat.toIsometry_inv_rightUnitor`, `QuadraticModuleCat.toIsometry_inv_leftUnitor`, `CliffordAlgebra.equivOfIsometry_apply`, `QuadraticModuleCat.ofIso_inv`, `QuadraticModuleCat.hom_hom_associator`, `QuadraticModuleCat.hom_inv_associator`
`toLinearEquiv` 📖	CompOp	17 math math: `map_radical`, `prodProdProdComm_invFun`, `QuadraticForm.tensorAssoc_toLinearEquiv`, `QuadraticForm.dualProdIsometry_invFun`, `prodComm_invFun`, `QuadraticForm.tensorLId_toLinearEquiv`, `map_posDef_iff`, `QuadraticForm.tensorComm_toLinearEquiv`, `QuadraticForm.tensorRId_toLinearEquiv`, `coe_toLinearEquiv`, `CategoryTheory.Iso.toIsometryEquiv_invFun`, `map_app'`, `map_negDef_iff`, `pi_toLinearEquiv`, `prod_toLinearEquiv`, `QuadraticForm.dualProdProdIsometry_invFun`, `coe_symm_toLinearEquiv`
`trans` 📖	CompOp	3 math math: `CliffordAlgebra.equivOfIsometry_trans`, `QuadraticModuleCat.ofIso_trans`, `CategoryTheory.Iso.toIsometryEquiv_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_symm_apply` `RingHomInvPair.ids`
`coe_symm_toLinearEquiv` 📖	mathematical	—	`LinearEquiv.symm` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `toLinearEquiv` `symm`	—	`RingHomInvPair.ids`
`coe_toLinearEquiv` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLinearEquiv` `QuadraticMap.IsometryEquiv` `instEquivLike`	—	`RingHomInvPair.ids`
`instLinearEquivClass` 📖	mathematical	—	`LinearEquivClass` `QuadraticMap.IsometryEquiv` `CommSemiring.toSemiring` `instEquivLike`	—	`RingHomInvPair.ids` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `MulActionSemiHomClass.map_smulₛₗ` `SemilinearMapClass.toMulActionSemiHomClass`
`map_app` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `QuadraticMap.instFunLike` `QuadraticMap.IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`map_app'`
`map_app'` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `QuadraticMap.instFunLike` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `toLinearEquiv`	—	—
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_apply` `RingHomInvPair.ids`
`toIsometry_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `QuadraticMap.Isometry.instFunLike` `toIsometry` `QuadraticMap.IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	—

(root)

Definitions

Name	Category	Theorems
`IsometryEquiv` 📖	CompData	133 math math: `IsometryEquiv.image_sphere`, `EuclideanGeometry.euclideanHausdorffMeasure_eq`, `IsometryEquiv.image_emetric_closedBall`, `IsometryEquiv.dimH_preimage`, `LinearIsometryEquiv.coe_symm_toIsometryEquiv`, `IsometryEquiv.preimage_sphere`, `IsometryEquiv.toRealLinearIsometryEquiv_symm_apply`, `IsometryEquiv.range_eq_univ`, `IsometryEquiv.apply_symm_apply`, `IsometryEquiv.withLpUniqueProd_symm_apply`, `IsometryEquiv.subLeft_symm_apply`, `IsometryEquiv.toRealLinearIsometryEquiv_apply`, `IsometryEquiv.withLpProdUnique_apply`, `IsometryEquiv.neg_apply`, `IsometryEquiv.midpoint_fixed`, `IsometryEquiv.preimage_emetric_closedBall`, `GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv`, `IsometryEquiv.coe_toHomeomorph`, `IsometryEquiv.inv_apply_self`, `IsometryEquiv.piCongrLeft'_apply`, `IsometryEquiv.constVSub_symm_apply`, `IsometryEquiv.image_emetric_ball`, `IsometryEquiv.divLeft_apply`, `IsometryEquiv.subRight_apply`, `IsometryEquiv.image_closedEBall`, `IsometryEquiv.symm_apply_apply`, `Fin.appendIsometry_symm_apply`, `IsometryEquiv.diam_image`, `IsometryEquiv.edist_eq`, `IsometryEquiv.hausdorffMeasure_image`, `LinearIsometryEquiv.toIsometryEquiv_injective`, `IsometryEquiv.ediam_preimage`, `Delone.DeloneSet.mapIsometry_symm_apply_carrier`, `IsometryEquiv.preimage_emetric_ball`, `IsometryEquiv.comp_continuousOn_iff`, `IsometryEquiv.image_eball`, `IsometryEquiv.ext_iff`, `Fin.appendIsometryOfEq_apply`, `IsometryEquiv.divRight_apply`, `IsometryEquiv.divLeft_symm_apply`, `IsometryEquiv.instIsometryClass`, `IsometryEquiv.preimage_closedEBall`, `IsometryEquiv.mulLeft_apply`, `IsometryEquiv.map_midpoint`, `IsometryEquiv.addLeft_apply`, `LinearIsometryEquiv.coe_toIsometryEquiv`, `IsometryEquiv.coe_withLpProdUnique`, `IsometryEquiv.map_hausdorffMeasure`, `IsometryEquiv.bijective`, `IsometryEquiv.piFinTwo_symm_apply`, `IsometryEquiv.hausdorffMeasure_preimage`, `IsometryEquiv.sumArrowIsometryEquivProdArrow_symm_apply`, `IsometryEquiv.withLpProdCongr_apply`, `IsometryEquiv.piCongrLeft_symm_apply`, `IsometryEquiv.ediam_image`, `Isometry.isometryEquivOnRange_apply`, `IsometryEquiv.measurePreserving_hausdorffMeasure`, `IsometryEquiv.funUnique_apply`, `IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero`, `EuclideanGeometry.measurePreserving_vaddConst`, `IsometryEquiv.coe_withLpUniqueProd`, `IsometryEquiv.dimH_image`, `IsometryEquiv.diam_preimage`, `IsometryEquiv.toDilationEquiv_toDilation`, `IsometryEquiv.apply_inv_self`, `IsometryEquiv.coe_eq_toEquiv`, `AffineIsometryEquiv.coe_toIsometryEquiv`, `MeasureTheory.OuterMeasure.isometryEquiv_map_mkMetric`, `IsometryEquiv.addRight_apply`, `IsometryEquiv.comp_continuous_iff'`, `IsometryEquiv.piCongrLeft_apply`, `IsometryEquiv.coe_toEquiv`, `Fin.appendIsometryOfEq_symm_apply`, `IsometryEquiv.image_closedBall`, `IsometryEquiv.dist_eq`, `IsometryEquiv.vaddConst_apply`, `IsometryEquiv.toEquiv_injective`, `IsometryEquiv.withLpProdUnique_symm_apply`, `IsometryEquiv.piCongrLeft'_symm_apply`, `IsometryEquiv.withLpProdAssoc_apply`, `IsometryEquiv.withLpUniqueProd_apply`, `IsometryEquiv.symm_apply_eq`, `IsometryEquiv.toDilationEquiv_apply`, `IsometryEquiv.funUnique_symm_apply`, `IsometryEquiv.constVSub_apply`, `IsometryEquiv.coe_mul`, `IsometryEquiv.coeFn_toRealAffineIsometryEquiv`, `IsometryEquiv.coe_symm_toEquiv`, `IsometryEquiv.eq_symm_apply`, `IsometryEquiv.injective`, `IsometryEquiv.constVAdd_apply`, `IsometryEquiv.constSMul_apply`, `IsometryEquiv.image_symm`, `IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero_symm`, `IsometryEquiv.vaddConst_symm_apply`, `IsometryEquiv.piFinTwo_apply`, `IsometryEquiv.coe_one`, `IsometryEquiv.symm_bijective`, `IsometryEquiv.coe_symm_toDilationEquiv`, `Fin.appendIsometry_apply`, `IsometryEquiv.symm_comp_self`, `IsometryEquiv.mul_apply`, `IsometryEquiv.image_ball`, `IsometryEquiv.withLpProdAssoc_symm_apply`, `IsometryClass.toIsometryEquiv_injective`, `ContinuousMap.isometryEquivBoundedOfCompact_symm_apply`, `AffineIsometryEquiv.coe_symm_toIsometryEquiv`, `IsometryEquiv.nndist_eq`, `IsometryEquiv.mulRight_apply`, `IsometryEquiv.subLeft_apply`, `IsometryEquiv.coe_mk`, `IsometryEquiv.withLpProdCongr_symm_apply`, `IsometryEquiv.withLpProdComm_apply`, `ContinuousMap.isometryEquivBoundedOfCompact_apply`, `IsometryEquiv.measurePreserving_euclideanHausdorffMeasure`, `IsometryEquiv.continuous`, `IsometryEquiv.preimage_symm`, `IsometryEquiv.sumArrowIsometryEquivProdArrow_apply`, `IsometryEquiv.preimage_closedBall`, `IsometryEquiv.preimage_ball`, `IsometryEquiv.coe_toDilationEquiv`, `IsometryEquiv.coe_toHomeomorph_symm`, `IsometryEquiv.symm_trans_apply`, `IsometryEquiv.isometry`, `IsometryEquiv.surjective`, `IsometryEquiv.preimage_eball`, `IsometryEquiv.inv_apply`, `IsometryEquiv.trans_apply`, `Delone.DeloneSet.mapIsometry_apply_carrier`, `IsometryEquiv.self_comp_symm`, `IsometryEquiv.comp_continuous_iff`, `MeasureTheory.OuterMeasure.isometryEquiv_comap_mkMetric`, `IsometryClass.coe_coe`

---

← Back to Index