Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/AddTorsor/Basic.lean

Statistics

Metric	Count
Definitions `constVAddHom`, `instAddTorsor`, `instAddTorsor`	3
Theorems `constVAdd_add`, `constVAdd_zero`, `injective_pointReflection_left_of_injective_two_nsmul`, `left_vsub_pointReflection`, `pointReflection_eq_subLeft`, `pointReflection_fixed_iff_of_injective_two_nsmul`, `right_vsub_pointReflection`, `vsub_apply`, `vsub_def`, `fst_vadd`, `fst_vsub`, `mk_vadd_mk`, `mk_vsub_mk`, `snd_vadd`, `snd_vsub`, `singleton_vsub_self`, `vadd_set_vsub_vadd_set`, `sub_add_vsub_comm`, `vadd_eq_vadd_iff_sub_eq_vsub`, `vadd_vsub_vadd_cancel_left`, `vadd_vsub_vadd_comm`, `vsub_left_cancel`, `vsub_left_cancel_iff`, `vsub_left_injective`, `vsub_right_cancel`, `vsub_right_cancel_iff`, `vsub_right_injective`, `vsub_sub_vsub_cancel_left`, `vsub_sub_vsub_comm`, `vsub_vadd_comm`	30
Total	33

Equiv

Definitions

Name	Category	Theorems
`constVAddHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constVAdd_add` 📖	mathematical	—	`constVAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Perm` `Perm.instMul`	—	`ext` `AddSemigroupAction.add_vadd`
`constVAdd_zero` 📖	mathematical	—	`constVAdd` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Perm` `Perm.instOne`	—	`ext` `zero_vadd`
`injective_pointReflection_left_of_injective_two_nsmul` 📖	mathematical	`AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `pointReflection`	—	`vsub_eq_zero_iff_eq` `nsmul_zero` `two_nsmul` `neg_eq_iff_add_eq_zero` `neg_vsub_eq_vsub_rev` `vsub_sub_vsub_cancel_right` `vadd_eq_vadd_iff_sub_eq_vsub` `pointReflection_apply`
`left_vsub_pointReflection` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `pointReflection`	—	`neg_injective` `neg_vsub_eq_vsub_rev` `pointReflection_vsub_left`
`pointReflection_eq_subLeft` 📖	mathematical	—	`pointReflection` `AddCommGroup.toAddGroup` `addGroupIsAddTorsor` `subLeft` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Perm.ext` `sub_add_eq_add_sub` `two_nsmul`
`pointReflection_fixed_iff_of_injective_two_nsmul` 📖	mathematical	`AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `pointReflection`	—	`pointReflection_apply` `eq_vadd_iff_vsub_eq` `neg_vsub_eq_vsub_rev` `neg_eq_iff_add_eq_zero` `two_nsmul` `nsmul_zero` `vsub_eq_zero_iff_eq`
`right_vsub_pointReflection` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `pointReflection` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`neg_injective` `neg_vsub_eq_vsub_rev` `pointReflection_vsub_right`

Pi

Definitions

Name	Category	Theorems
`instAddTorsor` 📖	CompOp	15 math math: `AffineMap.pi_lineMap_apply`, `AffineMap.proj_linear`, `AffineMap.pi_apply`, `Filter.Tendsto.vsub`, `AffineMap.proj_apply`, `vsub_apply`, `vsub_def`, `AffineMap.proj_pi`, `LipschitzWith.vsub`, `pi_midpoint_apply`, `AffineMap.pi_comp`, `AffineMap.pi_eq_zero`, `AffineMap.pi_zero`, `AffineMap.pi_linear`, `instIsTopologicalAddTorsorForall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vsub_apply` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `addGroup` `instAddTorsor`	—	—
`vsub_def` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `addGroup` `instAddTorsor`	—	—

Prod

Definitions

Name	Category	Theorems
`instAddTorsor` 📖	CompOp	50 math math: `NumberField.mixedEmbedding.fundamentalDomain_integerLattice`, `ContinuousAffineEquiv.prodComm_apply`, `ContinuousAffineMap.prodMap_apply`, `instIsTopologicalAddTorsorProd`, `ContinuousAffineEquiv.prodCongr_toContinuousAffineMap`, `ContinuousAffineEquiv.prodAssoc_toAffineEquiv`, `AffineEquiv.prodComm_apply`, `ContinuousAffineMap.prodMap_toAffineMap`, `mk_vsub_mk`, `AffineEquiv.prodAssoc_symm_apply`, `ContinuousAffineEquiv.prodCongr_apply`, `ContinuousAffineEquiv.prodComm_symm_apply`, `NumberField.mixedEmbedding.fundamentalDomain_idealLattice`, `AffineEquiv.prodAssoc_apply`, `fst_vsub`, `AffineEquiv.linear_prodAssoc`, `ContinuousAffineEquiv.prodComm_toAffineEquiv`, `AffineMap.prod_linear`, `AffineEquiv.coe_prodCongr`, `ContinuousAffineMap.prod_contLinear`, `AffineMap.coe_fst`, `ContinuousAffineMap.prodMap_contLinear`, `AffineMap.fst_lineMap`, `AffineMap.prodMap_linear`, `AffineEquiv.prodCongr_apply`, `AffineMap.coe_prodMap`, `AffineMap.prod_apply`, `ContinuousAffineEquiv.prodCongr_symm`, `mk_vadd_mk`, `AffineMap.snd_lineMap`, `AffineEquiv.prodComm_symm`, `AffineEquiv.prodCongr_symm`, `AffineMap.prodMap_apply`, `AffineMap.snd_linear`, `ContinuousAffineEquiv.prodComm_symm`, `ContinuousAffineMap.prod_apply`, `AffineEquiv.linear_prodCongr`, `AffineMap.fst_linear`, `ContinuousAffineEquiv.prodAssoc_apply`, `ContinuousAffineEquiv.prodCongr_toAffineEquiv`, `snd_vadd`, `ContinuousAffineMap.prod_toAffineMap`, `snd_vsub`, `fst_vadd`, `ContinuousAffineEquiv.prodAssoc_symm_apply`, `ContinuousAffineMap.coe_prod`, `AffineMap.coe_snd`, `ContinuousAffineMap.coe_prodMap`, `AffineMap.coe_prod`, `AffineEquiv.linear_prodComm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `instAddGroup` `instAddTorsor`	—	—
`fst_vsub` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `instAddGroup` `instAddTorsor`	—	—
`mk_vadd_mk` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `instAddGroup` `instAddTorsor`	—	—
`mk_vsub_mk` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `instAddGroup` `instAddTorsor`	—	—
`snd_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `instAddGroup` `instAddTorsor`	—	—
`snd_vsub` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `instAddGroup` `instAddTorsor`	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`singleton_vsub_self` 📖	mathematical	—	`VSub.vsub` `Set` `vsub` `AddTorsor.toVSub` `instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`singleton_vsub_singleton` `vsub_self`
`vadd_set_vsub_vadd_set` 📖	mathematical	—	`VSub.vsub` `Set` `vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `HVAdd.hVAdd` `instHVAdd` `vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`ext` `vadd_vsub_vadd_cancel_left`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sub_add_vsub_comm` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `VSub.vsub` `AddTorsor.toVSub` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`vadd_vsub_vadd_comm`
`vadd_eq_vadd_iff_sub_eq_vsub` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `SubNegMonoid.toSub` `VSub.vsub` `AddTorsor.toVSub`	—	`vadd_eq_vadd_iff_neg_add_eq_vsub` `neg_add_eq_sub`
`vadd_vsub_vadd_cancel_left` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`vsub_vadd_eq_vsub_sub` `vadd_vsub_assoc` `add_sub_cancel_left`
`vadd_vsub_vadd_comm` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub`	—	`vsub_vadd_eq_vsub_sub` `vadd_vsub_assoc` `add_sub_assoc` `add_comm_sub`
`vsub_left_cancel` 📖	—	`VSub.vsub` `AddTorsor.toVSub`	—	—	`vsub_eq_zero_iff_eq` `vsub_sub_vsub_cancel_right` `sub_eq_zero`
`vsub_left_cancel_iff` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub`	—	`vsub_left_cancel`
`vsub_left_injective` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub`	—	`vsub_left_cancel`
`vsub_right_cancel` 📖	—	`VSub.vsub` `AddTorsor.toVSub`	—	—	`vadd_left_cancel` `vsub_vadd`
`vsub_right_cancel_iff` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub`	—	`vsub_right_cancel`
`vsub_right_injective` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub`	—	`vsub_right_cancel`
`vsub_sub_vsub_cancel_left` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `VSub.vsub` `AddTorsor.toVSub`	—	`sub_eq_add_neg` `neg_vsub_eq_vsub_rev` `add_comm` `vsub_add_vsub_cancel`
`vsub_sub_vsub_comm` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `VSub.vsub` `AddTorsor.toVSub`	—	`vsub_vadd_eq_vsub_sub` `vsub_vadd_comm`
`vsub_vadd_comm` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `VSub.vsub` `AddTorsor.toVSub`	—	`vsub_eq_zero_iff_eq` `vadd_vsub_assoc` `vsub_vadd_eq_vsub_sub` `vsub_sub_vsub_cancel_left` `vsub_add_vsub_cancel` `vsub_self`

---

← Back to Index