Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `fst`, `inl`, `inr`, `proj`, `single`, `snd`, `pi`, `prod`, `prodComm`, `prodProdProdComm`, `pi`, `prod`	12
Theorems `pi`, `prod`, `inl_inr`, `inr_inl`, `prod`, `fst_apply`, `fst_comp_inl`, `fst_comp_inr`, `inl_apply`, `inr_apply`, `proj_apply`, `proj_comp_single_of_ne`, `proj_comp_single_of_same`, `single_apply`, `snd_apply`, `snd_comp_inl`, `snd_comp_inr`, `pi_toLinearEquiv`, `prodComm_invFun`, `prodComm_toFun`, `prodProdProdComm_invFun`, `prodProdProdComm_toFun`, `prod_toLinearEquiv`, `prod`, `associated_pi`, `polarBilin_pi`, `polar_pi`, `anisotropic_of_pi`, `anisotropic_of_prod`, `associated_prod`, `isOrtho_inl_inl_iff`, `isOrtho_inr_inr_iff`, `nonneg_pi_iff`, `nonneg_prod_iff`, `pi_apply`, `pi_apply_single`, `polarBilin_prod`, `polar_prod`, `posDef_pi_iff`, `posDef_prod_iff`, `prod_apply`	41
Total	53

QuadraticMap

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	13 math math: `posDef_pi_iff`, `Isometry.proj_comp_single_of_same`, `Isometry.single_apply`, `Ring.polarBilin_pi`, `Isometry.proj_comp_single_of_ne`, `pi_apply_single`, `Isometry.proj_apply`, `pi_apply`, `Ring.associated_pi`, `nonneg_pi_iff`, `Equivalent.pi`, `IsometryEquiv.pi_toLinearEquiv`, `Ring.polar_pi`
`prod` 📖	CompOp	36 math math: `Isometry.inl_apply`, `polarBilin_prod`, `CliffordAlgebra.toProd_comp_ofProd`, `polar_prod`, `CliffordAlgebra.toProd_ι_tmul_one`, `IsOrtho.prod`, `associated_prod`, `IsometryEquiv.prodProdProdComm_invFun`, `isOrtho_inl_inl_iff`, `Isometry.snd_comp_inl`, `Isometry.snd_apply`, `prod_apply`, `IsometryEquiv.prodComm_invFun`, `IsOrtho.inr_inl`, `posDef_prod_iff`, `isOrtho_inr_inr_iff`, `Equivalent.prod`, `QuadraticForm.toDualProd_apply`, `Isometry.fst_apply`, `Isometry.fst_comp_inl`, `CliffordAlgebra.prodEquiv_symm_apply`, `CliffordAlgebra.prodEquiv_apply`, `CliffordAlgebra.ofProd_comp_toProd`, `Isometry.fst_comp_inr`, `IsometryEquiv.prodComm_toFun`, `QuadraticForm.dualProdProdIsometry_toFun`, `CliffordAlgebra.toProd_one_tmul_ι`, `IsometryEquiv.prodProdProdComm_toFun`, `Isometry.inr_apply`, `nonneg_prod_iff`, `CliffordAlgebra.ofProd_ι_mk`, `IsOrtho.inl_inr`, `IsometryEquiv.prod_toLinearEquiv`, `QuadraticForm.dualProdProdIsometry_invFun`, `PosDef.prod`, `Isometry.snd_comp_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anisotropic_of_pi` 📖	—	`Anisotropic` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `pi`	—	—	`pi_apply` `Finset.sum_eq_zero` `Pi.single_eq_same` `Pi.single_eq_of_ne` `map_zero` `zeroHomClass`
`anisotropic_of_prod` 📖	—	`Anisotropic` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `prod`	—	—	`zero_add` `map_zero` `zeroHomClass` `add_zero`
`associated_prod` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `QuadraticMap` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommGroup` `Prod.instModule` `LinearMap.BilinMap` `instAddCommMonoid` `LinearMap.addCommMonoid` `LinearMap.module` `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` `associated` `instInvertibleEndOfNat` `prod` `Prod.instAddCommMonoid` `LinearMap.instAdd` `LinearMap.compl₁₂` `LinearMap.fst` `LinearMap.snd`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `LinearMap.instSMulCommClass` `polarBilin_prod` `Module.End.apply_smulCommClass` `IsScalarTower.left` `smul_add`
`isOrtho_inl_inl_iff` 📖	mathematical	—	`IsOrtho` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`add_zero` `map_zero` `zeroHomClass`
`isOrtho_inr_inr_iff` 📖	mathematical	—	`IsOrtho` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`add_zero` `map_zero` `zeroHomClass` `zero_add`
`nonneg_pi_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `QuadraticMap` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `instFunLike` `pi`	—	`sum_apply` `Finset.sum_congr` `Finset.sum_eq_single_of_mem` `Finset.mem_univ` `Pi.single_eq_of_ne` `map_zero` `zeroHomClass` `Pi.single_eq_same` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono`
`nonneg_prod_iff` 📖	mathematical	—	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `QuadraticMap` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `instFunLike` `prod`	—	`map_zero` `zeroHomClass` `add_zero` `zero_add` `add_nonneg`
`pi_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `instFunLike` `pi` `Finset.sum` `Finset.univ`	—	`sum_apply`
`pi_apply_single` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `instFunLike` `pi` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`pi_apply` `Fintype.sum_eq_single` `Pi.single_eq_of_ne` `map_zero` `zeroHomClass` `Pi.single_eq_same`
`polarBilin_prod` 📖	mathematical	—	`polarBilin` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `prod` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `LinearMap.addCommMonoid` `LinearMap.module` `LinearMap.instAdd` `LinearMap.compl₁₂` `LinearMap.fst` `LinearMap.snd`	—	`LinearMap.ext₂` `polar_prod`
`polar_prod` 📖	mathematical	—	`polar` `Prod.instAddCommGroup` `DFunLike.coe` `QuadraticMap` `CommRing.toCommSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `instFunLike` `prod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg`
`posDef_pi_iff` 📖	mathematical	—	`PosDef` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `pi`	—	`anisotropic_of_pi` `Finset.sum_eq_zero_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `pi_apply` `Finset.mem_univ`
`posDef_prod_iff` 📖	mathematical	—	`PosDef` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `prod`	—	`anisotropic_of_prod` `Prod.mk_eq_zero` `Anisotropic.eq_zero_iff` `add_eq_zero_iff_of_nonneg` `covariant_swap_add_of_covariant_add`
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `instFunLike` `prod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—

QuadraticMap.Equivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi` 📖	mathematical	`QuadraticMap.Equivalent`	`Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `QuadraticMap.pi`	—	—
`prod` 📖	mathematical	—	`QuadraticMap.Equivalent` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod`	—	`Nonempty.map2`

QuadraticMap.IsOrtho

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl_inr` 📖	mathematical	—	`QuadraticMap.IsOrtho` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`prod` `zero_right` `zero_left`
`inr_inl` 📖	mathematical	—	`QuadraticMap.IsOrtho` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`symm` `inl_inr`
`prod` 📖	mathematical	`QuadraticMap.IsOrtho`	`Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod`	—	`add_add_add_comm`

QuadraticMap.Isometry

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	3 math math: `fst_apply`, `fst_comp_inl`, `fst_comp_inr`
`inl` 📖	CompOp	3 math math: `inl_apply`, `snd_comp_inl`, `fst_comp_inl`
`inr` 📖	CompOp	3 math math: `fst_comp_inr`, `inr_apply`, `snd_comp_inr`
`proj` 📖	CompOp	3 math math: `proj_comp_single_of_same`, `proj_comp_single_of_ne`, `proj_apply`
`single` 📖	CompOp	3 math math: `proj_comp_single_of_same`, `single_apply`, `proj_comp_single_of_ne`
`snd` 📖	CompOp	3 math math: `snd_comp_inl`, `snd_apply`, `snd_comp_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `QuadraticMap` `QuadraticMap.instZero` `instFunLike` `fst`	—	—
`fst_comp_inl` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `QuadraticMap` `QuadraticMap.instZero` `fst` `inl` `id`	—	`ext`
`fst_comp_inr` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap` `QuadraticMap.instZero` `QuadraticMap.prod` `fst` `inr` `QuadraticMap.Isometry` `instZeroOfNat`	—	`ext`
`inl_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `instFunLike` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`inr_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `instFunLike` `inr` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`proj_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `QuadraticMap.pi` `Pi.single` `QuadraticMap` `QuadraticMap.instZero` `instFunLike` `proj`	—	—
`proj_comp_single_of_ne` 📖	mathematical	—	`comp` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `Pi.single` `QuadraticMap` `QuadraticMap.instZero` `QuadraticMap.pi` `proj` `single` `QuadraticMap.Isometry` `instZeroOfNat` `ofEq` `Pi.single_eq_of_ne`	—	`ext` `Pi.single_eq_of_ne`
`proj_comp_single_of_same` 📖	mathematical	—	`comp` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `Pi.single` `QuadraticMap` `QuadraticMap.instZero` `QuadraticMap.pi` `proj` `single` `ofEq` `Pi.single_eq_same`	—	`ext` `Pi.single_eq_same`
`single_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `QuadraticMap.pi` `instFunLike` `single` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `QuadraticMap` `QuadraticMap.instZero` `instFunLike` `snd`	—	—
`snd_comp_inl` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap` `QuadraticMap.instZero` `QuadraticMap.prod` `snd` `inl` `QuadraticMap.Isometry` `instZeroOfNat`	—	`ext`
`snd_comp_inr` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `QuadraticMap` `QuadraticMap.instZero` `snd` `inr` `id`	—	`ext`

QuadraticMap.IsometryEquiv

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	1 math math: `pi_toLinearEquiv`
`prod` 📖	CompOp	1 math math: `prod_toLinearEquiv`
`prodComm` 📖	CompOp	2 math math: `prodComm_invFun`, `prodComm_toFun`
`prodProdProdComm` 📖	CompOp	2 math math: `prodProdProdComm_invFun`, `prodProdProdComm_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi_toLinearEquiv` 📖	mathematical	—	`toLinearEquiv` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `QuadraticMap.pi` `pi` `LinearEquiv.piCongrRight`	—	`RingHomInvPair.ids`
`prodComm_invFun` 📖	mathematical	—	`LinearEquiv.invFun` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `toLinearEquiv` `QuadraticMap.prod` `prodComm`	—	`RingHomInvPair.ids`
`prodComm_toFun` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `EquivLike.toFunLike` `instEquivLike` `prodComm`	—	—
`prodProdProdComm_invFun` 📖	mathematical	—	`LinearEquiv.invFun` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `toLinearEquiv` `QuadraticMap.prod` `prodProdProdComm`	—	`RingHomInvPair.ids`
`prodProdProdComm_toFun` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `EquivLike.toFunLike` `instEquivLike` `prodProdProdComm`	—	—
`prod_toLinearEquiv` 📖	mathematical	—	`toLinearEquiv` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod` `prod` `LinearEquiv.prodCongr`	—	`RingHomInvPair.ids`

QuadraticMap.PosDef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`QuadraticMap.PosDef`	`Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `QuadraticMap.prod`	—	`QuadraticMap.posDef_prod_iff`

QuadraticMap.Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associated_pi` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `QuadraticMap` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `Pi.module` `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.pi` `Finset.sum` `Pi.addCommMonoid` `Finset.univ` `LinearMap.compl₁₂` `LinearMap.proj`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `LinearMap.instSMulCommClass` `polarBilin_pi` `Module.End.apply_smulCommClass` `IsScalarTower.left` `Finset.smul_sum`
`polarBilin_pi` 📖	mathematical	—	`QuadraticMap.polarBilin` `Pi.addCommGroup` `Pi.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.pi` `Finset.sum` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `LinearMap.addCommMonoid` `LinearMap.module` `Finset.univ` `LinearMap.compl₁₂` `LinearMap.proj`	—	`LinearMap.ext₂` `polar_pi` `LinearMap.coe_sum` `Finset.sum_apply` `Finset.sum_congr`
`polar_pi` 📖	mathematical	—	`QuadraticMap.polar` `Pi.addCommGroup` `DFunLike.coe` `QuadraticMap` `CommRing.toCommSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.module` `CommSemiring.toSemiring` `QuadraticMap.instFunLike` `QuadraticMap.pi` `Finset.sum` `Finset.univ`	—	`Finset.sum_sub_distrib` `QuadraticMap.pi_apply` `Finset.sum_congr`

---

← Back to Index