MidpointZero

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

Statistics

Metric	Count
Definitions	0
Theorems homothety_invOf_two, homothety_inv_two, homothety_one_half, lineMap_inv_two, lineMap_one_half, pi_midpoint_apply	6
Total	6

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homothety_invOf_two 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing AffineMap.instFunLike AffineMap.homothety Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat midpoint	—	Nat.instAtLeastTwoHAddOfNat
homothety_inv_two 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing Field.toCommRing AffineMap.instFunLike AffineMap.homothety InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat midpoint invertibleTwo Semifield.toDivisionSemiring	—	Nat.instAtLeastTwoHAddOfNat
homothety_one_half 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing Field.toCommRing AffineMap.instFunLike AffineMap.homothety DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat midpoint invertibleTwo Semifield.toDivisionSemiring Field.toSemifield	—	Nat.instAtLeastTwoHAddOfNat one_div homothety_inv_two
lineMap_inv_two 📖	mathematical	—	DFunLike.coe AffineMap DivisionRing.toRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat midpoint invertibleTwo	—	Nat.instAtLeastTwoHAddOfNat
lineMap_one_half 📖	mathematical	—	DFunLike.coe AffineMap DivisionRing.toRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat midpoint invertibleTwo DivisionRing.toDivisionSemiring	—	Nat.instAtLeastTwoHAddOfNat one_div lineMap_inv_two
pi_midpoint_apply 📖	mathematical	—	midpoint Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup	—	Nat.instAtLeastTwoHAddOfNat

---

← Back to Index