Fin

📁 Source: Mathlib/Algebra/Ring/Fin.lean

Statistics

Metric	Count
Definitions piFinTwo	1
Theorems piFinTwo_apply, piFinTwo_symm_apply	2
Total	3

RingEquiv

Definitions

Name	Category	Theorems
piFinTwo 📖	CompOp	2 math math: piFinTwo_symm_apply, piFinTwo_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piFinTwo_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Prod.instMul Pi.instAdd Distrib.toAdd Prod.instAdd EquivLike.toFunLike instEquivLike piFinTwo Equiv Equiv.instEquivLike piFinTwoEquiv	—	—
piFinTwo_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.instMul Prod.instAdd Distrib.toAdd Pi.instAdd EquivLike.toFunLike instEquivLike symm piFinTwo Equiv.invFun piFinTwoEquiv	—	—

---

← Back to Index