Documentation Verification Report

Involutions

📁 Source: PhysLean/Mathematics/Fin/Involutions.lean

Statistics

Metric	Count
Definitions `instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean`, `involutionAddEquiv`, `involutionCons`, `involutionNoFixedEquivSum`, `involutionNoFixedEquivSumSame`, `involutionNoFixedSetOne`, `involutionNoFixedZeroEquivProd`, `involutionNoFixedZeroSetEquiv`, `involutionNoFixedZeroSetEquivEquiv`, `involutionNoFixedZeroSetEquivEquiv'`, `involutionNoFixedZeroSetEquivSetEquiv`, `involutionNoFixedZeroSetEquivSetOne`	12
Theorems `involutionAddEquiv_cast`, `involutionAddEquiv_cast'`, `involutionAddEquiv_none_image_zero`, `involutionAddEquiv_none_succ`, `involutionCons_ext`, `involutionNoFixed_card_even`, `involutionNoFixed_card_mul_two`, `involutionNoFixed_card_mul_two_plus_one`, `involutionNoFixed_card_odd`, `involutionNoFixed_card_succ`	10
Total	22

PhysLean.Fin

Definitions

Name	Category	Theorems
`instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean` 📖	CompOp	5 math math: `involutionNoFixed_card_mul_two`, `involutionNoFixed_card_succ`, `involutionNoFixed_card_odd`, `involutionNoFixed_card_even`, `involutionNoFixed_card_mul_two_plus_one`
`involutionAddEquiv` 📖	CompOp	2 math math: `involutionAddEquiv_cast'`, `involutionAddEquiv_cast`
`involutionCons` 📖	CompOp	—
`involutionNoFixedEquivSum` 📖	CompOp	—
`involutionNoFixedEquivSumSame` 📖	CompOp	—
`involutionNoFixedSetOne` 📖	CompOp	—
`involutionNoFixedZeroEquivProd` 📖	CompOp	—
`involutionNoFixedZeroSetEquiv` 📖	CompOp	—
`involutionNoFixedZeroSetEquivEquiv` 📖	CompOp	—
`involutionNoFixedZeroSetEquivEquiv'` 📖	CompOp	—
`involutionNoFixedZeroSetEquivSetEquiv` 📖	CompOp	—
`involutionNoFixedZeroSetEquivSetOne` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`involutionAddEquiv_cast` 📖	mathematical	—	`involutionAddEquiv`	—	—
`involutionAddEquiv_cast'` 📖	mathematical	—	`involutionAddEquiv`	—	—
`involutionAddEquiv_none_image_zero` 📖	—	`involutionCons` `involutionAddEquiv`	—	—	—
`involutionAddEquiv_none_succ` 📖	—	`involutionCons` `involutionAddEquiv`	—	—	`involutionAddEquiv_none_image_zero`
`involutionCons_ext` 📖	—	—	—	—	—
`involutionNoFixed_card_even` 📖	mathematical	—	`instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean`	—	`involutionNoFixed_card_mul_two`
`involutionNoFixed_card_mul_two` 📖	mathematical	—	`instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean`	—	`involutionNoFixed_card_succ`
`involutionNoFixed_card_mul_two_plus_one` 📖	mathematical	—	`instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean`	—	`involutionNoFixed_card_succ`
`involutionNoFixed_card_odd` 📖	mathematical	—	`instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean`	—	`involutionNoFixed_card_mul_two_plus_one`
`involutionNoFixed_card_succ` 📖	mathematical	—	`instFintypeSubtypeForallFinAndInvolutiveForallNe_physLean`	—	—

---

← Back to Index