Documentation Verification Report

Isometry

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

Statistics

Metric	Count
Definitions `apply`, `comp`, `hasZeroOfSubsingleton`, `id`, `instFunLike`, `instZeroOfNat`, `ofEq`, `toLinearMap`, `«term_→qᵢ_»`	9
Theorems `coe_toLinearMap`, `comp_apply`, `comp_assoc`, `comp_id`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instLinearMapClass`, `instSubsingleton`, `map_app`, `map_app'`, `ofEq_apply`, `ofEq_rfl`, `toLinearMap_comp`, `toLinearMap_injective`	16
Total	25

QuadraticMap.Isometry

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	13 math math: `QuadraticModuleCat.toIsometry_comp`, `proj_comp_single_of_same`, `snd_comp_inl`, `comp_apply`, `id_comp`, `proj_comp_single_of_ne`, `fst_comp_inl`, `fst_comp_inr`, `comp_assoc`, `comp_id`, `toLinearMap_comp`, `CliffordAlgebra.map_comp_map`, `snd_comp_inr`
`hasZeroOfSubsingleton` 📖	CompOp	—
`id` 📖	CompOp	10 math math: `CliffordAlgebra.map_id`, `ofEq_rfl`, `id_comp`, `QuadraticModuleCat.toIsometry_whiskerRight`, `QuadraticModuleCat.toIsometry_whiskerLeft`, `fst_comp_inl`, `QuadraticModuleCat.toIsometry_id`, `id_apply`, `comp_id`, `snd_comp_inr`
`instFunLike` 📖	CompOp	23 math math: `ext_iff`, `inl_apply`, `single_apply`, `QuadraticModuleCat.forget₂_map_associator_inv`, `QuadraticModuleCat.forget₂_map`, `CategoryTheory.Iso.toIsometryEquiv_toFun`, `QuadraticMap.IsometryEquiv.toIsometry_apply`, `snd_apply`, `CliffordAlgebra.map_apply_ι`, `comp_apply`, `map_app`, `QuadraticModuleCat.forget₂_map_associator_hom`, `QuadraticModuleCat.forget₂_obj`, `instLinearMapClass`, `QuadraticForm.toDualProd_apply`, `proj_apply`, `fst_apply`, `CategoryTheory.Iso.toIsometryEquiv_invFun`, `inr_apply`, `tmul_apply`, `id_apply`, `ofEq_apply`, `coe_toLinearMap`
`instZeroOfNat` 📖	CompOp	3 math math: `snd_comp_inl`, `proj_comp_single_of_ne`, `fst_comp_inr`
`ofEq` 📖	CompOp	4 math math: `proj_comp_single_of_same`, `ofEq_rfl`, `proj_comp_single_of_ne`, `ofEq_apply`
`toLinearMap` 📖	CompOp	10 math math: `CliffordAlgebra.ι_range_map_map`, `QuadraticForm.tmul_tensorMap_apply`, `QuadraticModuleCat.forget₂_map`, `QuadraticForm.tmul_comp_tensorMap`, `CliffordAlgebra.map_comp_ι`, `map_app'`, `toLinearMap_injective`, `tmul_apply`, `coe_toLinearMap`, `toLinearMap_comp`
`«term_→qᵢ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `toLinearMap` `QuadraticMap.Isometry` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	`ext`
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`ext` 📖	—	`DFunLike.coe` `QuadraticMap.Isometry` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instLinearMapClass` 📖	mathematical	—	`LinearMapClass` `QuadraticMap.Isometry` `CommSemiring.toSemiring` `instFunLike`	—	`LinearMap.map_add` `LinearMap.map_smul`
`instSubsingleton` 📖	mathematical	—	`QuadraticMap.Isometry`	—	`ext`
`map_app` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `QuadraticMap.instFunLike` `QuadraticMap.Isometry` `instFunLike`	—	`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` `toLinearMap`	—	—
`ofEq_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `instFunLike` `ofEq`	—	—
`ofEq_rfl` 📖	mathematical	—	`ofEq` `QuadraticMap` `id`	—	—
`toLinearMap_comp` 📖	mathematical	—	`toLinearMap` `comp` `LinearMap.comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	—
`toLinearMap_injective` 📖	mathematical	—	`QuadraticMap.Isometry` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap`	—	`DFunLike.coe_injective`

QuadraticMap.Isometry.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

---

← Back to Index