Documentation Verification Report

Pointwise

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

Statistics

Metric	Count
Definitions `mulAction`, `pointwiseAddAction`, `pointwiseSMul`, `pointwiseVAdd`	4
Theorems `coe_pointwise_vadd`, `coe_smul`, `direction_smul`, `map_pointwise_vadd`, `pointwise_vadd_bot`, `pointwise_vadd_direction`, `pointwise_vadd_eq_map`, `pointwise_vadd_span`, `pointwise_vadd_top`, `smul_bot`, `smul_eq_map`, `smul_mem_smul_iff`, `smul_mem_smul_iff_of_isUnit`, `smul_mem_smul_iff₀`, `smul_span`, `smul_top`, `vadd_mem_pointwise_vadd_iff`	17
Total	21

AffineSubspace

Definitions

Name	Category	Theorems
`mulAction` 📖	CompOp	—
`pointwiseAddAction` 📖	CompOp	—
`pointwiseSMul` 📖	CompOp	9 math math: `smul_mem_smul_iff₀`, `coe_smul`, `smul_bot`, `smul_top`, `smul_mem_smul_iff_of_isUnit`, `smul_eq_map`, `smul_mem_smul_iff`, `direction_smul`, `smul_span`
`pointwiseVAdd` 📖	CompOp	8 math math: `map_pointwise_vadd`, `coe_pointwise_vadd`, `pointwise_vadd_direction`, `pointwise_vadd_eq_map`, `pointwise_vadd_bot`, `pointwise_vadd_top`, `vadd_mem_pointwise_vadd_iff`, `pointwise_vadd_span`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_pointwise_vadd` 📖	mathematical	—	`SetLike.coe` `AffineSubspace` `instSetLike` `HVAdd.hVAdd` `instHVAdd` `pointwiseVAdd` `Set` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	—
`coe_smul` 📖	mathematical	—	`SetLike.coe` `AffineSubspace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instSetLike` `pointwiseSMul` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass`	—	—
`direction_smul` 📖	mathematical	—	`direction` `DivisionRing.toRing` `Field.toDivisionRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineSubspace` `pointwiseSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self` `LinearMap.ext` `RingHomSurjective.ids` `map_direction` `Submodule.map_smul` `Submodule.map_id`
`map_pointwise_vadd` 📖	mathematical	—	`map` `HVAdd.hVAdd` `AffineSubspace` `instHVAdd` `pointwiseVAdd` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `AffineMap.linear`	—	`pointwise_vadd_eq_map` `map_map` `AffineMap.ext` `AffineMap.map_vadd`
`pointwise_vadd_bot` 📖	mathematical	—	`HVAdd.hVAdd` `AffineSubspace` `instHVAdd` `pointwiseVAdd` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`ext` `map_bot`
`pointwise_vadd_direction` 📖	mathematical	—	`direction` `HVAdd.hVAdd` `AffineSubspace` `instHVAdd` `pointwiseVAdd`	—	`pointwise_vadd_eq_map` `RingHomSurjective.ids` `map_direction` `Submodule.map_id`
`pointwise_vadd_eq_map` 📖	mathematical	—	`HVAdd.hVAdd` `AffineSubspace` `instHVAdd` `pointwiseVAdd` `map` `AffineEquiv.toAffineMap` `AffineEquiv.constVAdd`	—	—
`pointwise_vadd_span` 📖	mathematical	—	`HVAdd.hVAdd` `AffineSubspace` `instHVAdd` `pointwiseVAdd` `affineSpan` `Set` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`map_span`
`pointwise_vadd_top` 📖	mathematical	—	`HVAdd.hVAdd` `AffineSubspace` `instHVAdd` `pointwiseVAdd` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`ext`
`smul_bot` 📖	mathematical	—	`AffineSubspace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `pointwiseSMul` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`ext` `map_bot`
`smul_eq_map` 📖	mathematical	—	`AffineSubspace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `pointwiseSMul` `map` `LinearMap.toAffineMap` `DistribSMul.toLinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	—
`smul_mem_smul_iff` 📖	mathematical	—	`AffineSubspace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SetLike.instMembership` `instSetLike` `pointwiseSMul` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass`	—	`Set.smul_mem_smul_set_iff`
`smul_mem_smul_iff_of_isUnit` 📖	mathematical	`IsUnit`	`AffineSubspace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SetLike.instMembership` `instSetLike` `pointwiseSMul` `DistribMulAction.toDistribSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass`	—	`smul_mem_smul_iff` `Units.smulCommClass_left`
`smul_mem_smul_iff₀` 📖	mathematical	—	`AffineSubspace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SetLike.instMembership` `instSetLike` `pointwiseSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass`	—	`smul_mem_smul_iff_of_isUnit` `Ne.isUnit`
`smul_span` 📖	mathematical	—	`AffineSubspace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `pointwiseSMul` `affineSpan` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass`	—	`map_span`
`smul_top` 📖	mathematical	`IsUnit`	`AffineSubspace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `pointwiseSMul` `DistribMulAction.toDistribSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`ext` `smul_inv_smul`
`vadd_mem_pointwise_vadd_iff` 📖	mathematical	—	`AffineSubspace` `SetLike.instMembership` `instSetLike` `HVAdd.hVAdd` `instHVAdd` `pointwiseVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`Set.vadd_mem_vadd_set_iff`

---

← Back to Index