Basic

📁 Source: Mathlib/Logic/Equiv/Fin/Basic.lean

Statistics

Metric	Count
Definitions `embeddingFinSucc`, `appendEquiv`, `castLEquiv`, `succFunEquiv`, `divModEquiv`, `divModEquiv`, `finAddFlip`, `finProdFinEquiv`, `finSuccAboveEquiv`, `finSuccEquiv`, `finSuccEquiv'`, `finSuccEquivLast`, `finSumFinEquiv`, `finSumNatEquiv`, `finTwoArrowEquiv`, `prodEquivPiFinTwo`	16
Theorems `coe_embeddingFinSucc_symm`, `embeddingFinSucc_fst`, `embeddingFinSucc_snd`, `appendEquiv_apply`, `appendEquiv_symm_apply`, `castLEquiv_apply`, `castLEquiv_symm_apply`, `preimage_apply_01_prod`, `preimage_apply_01_prod'`, `succFunEquiv_apply`, `succFunEquiv_symm_apply`, `divModEquiv_apply`, `divModEquiv_symm_apply`, `divModEquiv_apply`, `divModEquiv_symm_apply`, `finAddFlip_apply_castAdd`, `finAddFlip_apply_mk_left`, `finAddFlip_apply_mk_right`, `finAddFlip_apply_natAdd`, `finProdFinEquiv_apply_val`, `finProdFinEquiv_symm_apply`, `finSuccAboveEquiv_apply`, `finSuccAboveEquiv_symm_apply_last`, `finSuccAboveEquiv_symm_apply_ne_last`, `finSuccEquiv'_above`, `finSuccEquiv'_at`, `finSuccEquiv'_below`, `finSuccEquiv'_eq_none`, `finSuccEquiv'_eq_some`, `finSuccEquiv'_last_apply`, `finSuccEquiv'_last_apply_castSucc`, `finSuccEquiv'_ne_last_apply`, `finSuccEquiv'_succAbove`, `finSuccEquiv'_symm_coe_above`, `finSuccEquiv'_symm_coe_below`, `finSuccEquiv'_symm_none`, `finSuccEquiv'_symm_some`, `finSuccEquiv'_symm_some_above`, `finSuccEquiv'_symm_some_below`, `finSuccEquiv'_zero`, `finSuccEquivLast_castSucc`, `finSuccEquivLast_last`, `finSuccEquivLast_symm_none`, `finSuccEquivLast_symm_some`, `finSuccEquiv_eq_none`, `finSuccEquiv_eq_some`, `finSuccEquiv_succ`, `finSuccEquiv_symm_none`, `finSuccEquiv_symm_some`, `finSuccEquiv_zero`, `finSumFinEquiv_apply_left`, `finSumFinEquiv_apply_right`, `finSumFinEquiv_symm_apply_castAdd`, `finSumFinEquiv_symm_apply_castSucc`, `finSumFinEquiv_symm_apply_natAdd`, `finSumFinEquiv_symm_last`, `finSumNatEquiv_apply_left`, `finSumNatEquiv_apply_right`, `finSumNatEquiv_symm_apply_add_left`, `finSumNatEquiv_symm_apply_add_right`, `finSumNatEquiv_symm_apply_fin`, `finSumNatEquiv_symm_apply_of_ge`, `finSumNatEquiv_symm_apply_of_lt`, `finTwoArrowEquiv_apply`, `finTwoArrowEquiv_symm_apply`, `isLeft_finSumNatEquiv_symm_apply`, `isRight_finSumNatEquiv_symm_apply`, `prodEquivPiFinTwo_apply`, `prodEquivPiFinTwo_symm_apply`	69
Total	85

Equiv

Definitions

Name	Category	Theorems
`embeddingFinSucc` 📖	CompOp	3 math math: `embeddingFinSucc_snd`, `embeddingFinSucc_fst`, `coe_embeddingFinSucc_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_embeddingFinSucc_symm` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Equiv` `Set` `Set.instMembership` `Set.range` `EquivLike.toFunLike` `instEquivLike` `symm` `embeddingFinSucc` `Fin.cons`	—	—
`embeddingFinSucc_fst` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Set` `Set.instMembership` `Set.range` `Equiv` `EquivLike.toFunLike` `instEquivLike` `embeddingFinSucc`	—	—
`embeddingFinSucc_snd` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Equiv` `EquivLike.toFunLike` `instEquivLike` `embeddingFinSucc`	—	—

Fin

Definitions

Name	Category	Theorems
`appendEquiv` 📖	CompOp	3 math math: `appendHomeomorph_toEquiv`, `appendEquiv_symm_apply`, `appendEquiv_apply`
`castLEquiv` 📖	CompOp	2 math math: `castLEquiv_symm_apply`, `castLEquiv_apply`
`succFunEquiv` 📖	CompOp	2 math math: `succFunEquiv_symm_apply`, `succFunEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`appendEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `appendEquiv` `append`	—	—
`appendEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `appendEquiv`	—	—
`castLEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `castLEquiv`	—	—
`castLEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `castLEquiv`	—	—
`preimage_apply_01_prod` 📖	mathematical	—	`Set.preimage` `SProd.sprod` `Set` `Set.instSProd` `Set.pi` `Set.univ` `cons` `finZeroElim`	—	`Set.ext` `cons_zero` `cons_one`
`preimage_apply_01_prod'` 📖	mathematical	—	`Set.preimage` `SProd.sprod` `Set` `Set.instSProd` `Set.pi` `Set.univ` `Matrix.vecCons` `Matrix.vecEmpty`	—	`preimage_apply_01_prod`
`succFunEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `succFunEquiv`	—	—
`succFunEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `succFunEquiv` `append` `uniqueElim` `instUnique`	—	—

Int

Definitions

Name	Category	Theorems
`divModEquiv` 📖	CompOp	2 math math: `divModEquiv_apply`, `divModEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divModEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `divModEquiv` `natMod`	—	—
`divModEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `divModEquiv`	—	—

Nat

Definitions

Name	Category	Theorems
`divModEquiv` 📖	CompOp	2 math math: `divModEquiv_apply`, `divModEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divModEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `divModEquiv`	—	—
`divModEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `divModEquiv`	—	—

(root)

Definitions

Name	Category	Theorems
`finAddFlip` 📖	CompOp	5 math math: `finAddFlip_apply_mk_right`, `finRotate_succ`, `finAddFlip_apply_mk_left`, `finAddFlip_apply_natAdd`, `finAddFlip_apply_castAdd`
`finProdFinEquiv` 📖	CompOp	2 math math: `finProdFinEquiv_symm_apply`, `finProdFinEquiv_apply_val`
`finSuccAboveEquiv` 📖	CompOp	4 math math: `finSuccAboveEquiv_symm_apply_ne_last`, `finSuccAboveEquiv_symm_apply_last`, `finSuccAboveEquiv_apply`, `finSuccAboveOrderIso_symm_apply_ne_last`
`finSuccEquiv` 📖	CompOp	8 math math: `finSuccEquiv_zero`, `finSuccEquiv_symm_none`, `finSuccEquiv_succ`, `finSuccEquiv'_zero`, `finSuccEquiv_symm_some`, `finSuccEquiv_eq_some`, `finSuccEquiv_eq_none`, `MvPolynomial.finSuccEquiv_rename_finSuccEquiv`
`finSuccEquiv'` 📖	CompOp	16 math math: `finSuccEquiv'_eq_some`, `finSuccEquiv'_symm_coe_above`, `finSuccEquiv'_zero`, `finSuccEquiv'_at`, `finSuccEquiv'_ne_last_apply`, `finSuccEquiv'_below`, `finSuccEquiv'_symm_some_below`, `finSuccEquiv'_above`, `finSuccEquiv'_last_apply`, `finSuccEquiv'_symm_none`, `finSuccEquiv'_symm_coe_below`, `finSuccEquiv'_succAbove`, `finSuccEquiv'_eq_none`, `finSuccEquiv'_symm_some`, `finSuccEquiv'_symm_some_above`, `finSuccEquiv'_last_apply_castSucc`
`finSuccEquivLast` 📖	CompOp	4 math math: `finSuccEquivLast_castSucc`, `finSuccEquivLast_last`, `finSuccEquivLast_symm_none`, `finSuccEquivLast_symm_some`
`finSumFinEquiv` 📖	CompOp	10 math math: `finSumFinEquiv_apply_left`, `Polynomial.toMatrix_sylvesterMap'`, `Polynomial.sylvester_comm`, `finSumFinEquiv_apply_right`, `finSumFinEquiv_symm_apply_castAdd`, `MvPolynomial.universalFactorizationMapPresentation_map`, `finSumFinEquiv_symm_last`, `finSumFinEquiv_symm_apply_natAdd`, `finSumFinEquiv_symm_apply_castSucc`, `Polynomial.toMatrix_sylvesterMap`
`finSumNatEquiv` 📖	CompOp	9 math math: `isRight_finSumNatEquiv_symm_apply`, `finSumNatEquiv_symm_apply_fin`, `finSumNatEquiv_apply_left`, `finSumNatEquiv_symm_apply_add_left`, `isLeft_finSumNatEquiv_symm_apply`, `finSumNatEquiv_symm_apply_add_right`, `finSumNatEquiv_symm_apply_of_ge`, `finSumNatEquiv_symm_apply_of_lt`, `finSumNatEquiv_apply_right`
`finTwoArrowEquiv` 📖	CompOp	4 math math: `finTwoArrowEquiv_symm_apply`, `finTwoArrowEquiv_apply`, `Function.OfArity.uncurry_two_eq_uncurry`, `Function.OfArity.curry_two_eq_curry`
`prodEquivPiFinTwo` 📖	CompOp	2 math math: `prodEquivPiFinTwo_apply`, `prodEquivPiFinTwo_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finAddFlip_apply_castAdd` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finAddFlip`	—	`finSumFinEquiv_symm_apply_castAdd`
`finAddFlip_apply_mk_left` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finAddFlip`	—	`finAddFlip_apply_castAdd`
`finAddFlip_apply_mk_right` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finAddFlip`	—	`finAddFlip_apply_natAdd`
`finAddFlip_apply_natAdd` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finAddFlip`	—	`finSumFinEquiv_symm_apply_natAdd`
`finProdFinEquiv_apply_val` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finProdFinEquiv`	—	—
`finProdFinEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finProdFinEquiv`	—	—
`finSuccAboveEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccAboveEquiv` `Fin.succAbove` `Fin.succAbove_ne`	—	—
`finSuccAboveEquiv_symm_apply_last` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccAboveEquiv`	—	`Equiv.optionSubtype_apply_symm_apply` `Fin.succAbove_last`
`finSuccAboveEquiv_symm_apply_ne_last` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccAboveEquiv` `Fin.predAbove`	—	`Equiv.optionSubtype_apply_symm_apply` `finSuccEquiv'_ne_last_apply`
`finSuccEquiv'_above` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'`	—	`Fin.succAbove_of_le_castSucc` `finSuccEquiv'_succAbove`
`finSuccEquiv'_at` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'`	—	`Fin.insertNth_apply_same`
`finSuccEquiv'_below` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'`	—	`Fin.succAbove_of_castSucc_lt` `finSuccEquiv'_succAbove`
`finSuccEquiv'_eq_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`finSuccEquiv'_eq_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'` `Fin.succAbove`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`finSuccEquiv'_last_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'`	—	`Fin.succAbove_last`
`finSuccEquiv'_last_apply_castSucc` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'`	—	`Fin.succAbove_last` `finSuccEquiv'_succAbove`
`finSuccEquiv'_ne_last_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'` `Fin.predAbove`	—	`Fin.exists_succAbove_eq` `finSuccEquiv'_succAbove` `Fin.predAbove_succAbove`
`finSuccEquiv'_succAbove` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv'` `Fin.succAbove`	—	`Fin.insertNth_apply_succAbove`
`finSuccEquiv'_symm_coe_above` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquiv'`	—	`finSuccEquiv'_symm_some_above`
`finSuccEquiv'_symm_coe_below` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquiv'`	—	—
`finSuccEquiv'_symm_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquiv'`	—	—
`finSuccEquiv'_symm_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquiv'` `Fin.succAbove`	—	—
`finSuccEquiv'_symm_some_above` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquiv'`	—	`Fin.succAbove_of_le_castSucc`
`finSuccEquiv'_symm_some_below` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquiv'`	—	`Fin.succAbove_of_castSucc_lt`
`finSuccEquiv'_zero` 📖	mathematical	—	`finSuccEquiv'` `finSuccEquiv`	—	—
`finSuccEquivLast_castSucc` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquivLast`	—	—
`finSuccEquivLast_last` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquivLast`	—	`finSuccEquiv'_at`
`finSuccEquivLast_symm_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquivLast`	—	`finSuccEquiv'_symm_none`
`finSuccEquivLast_symm_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquivLast`	—	—
`finSuccEquiv_eq_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`finSuccEquiv_eq_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`finSuccEquiv_succ` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv`	—	`finSuccEquiv'_above`
`finSuccEquiv_symm_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquiv`	—	`finSuccEquiv'_symm_none`
`finSuccEquiv_symm_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccEquiv`	—	`Fin.succAbove_zero`
`finSuccEquiv_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSuccEquiv`	—	—
`finSumFinEquiv_apply_left` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSumFinEquiv`	—	—
`finSumFinEquiv_apply_right` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSumFinEquiv`	—	—
`finSumFinEquiv_symm_apply_castAdd` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumFinEquiv`	—	`Equiv.symm_apply_apply`
`finSumFinEquiv_symm_apply_castSucc` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumFinEquiv`	—	`finSumFinEquiv_symm_apply_castAdd`
`finSumFinEquiv_symm_apply_natAdd` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumFinEquiv`	—	`Equiv.symm_apply_apply`
`finSumFinEquiv_symm_last` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumFinEquiv`	—	`finSumFinEquiv_symm_apply_natAdd`
`finSumNatEquiv_apply_left` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSumNatEquiv`	—	—
`finSumNatEquiv_apply_right` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finSumNatEquiv`	—	—
`finSumNatEquiv_symm_apply_add_left` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumNatEquiv`	—	`finSumNatEquiv_symm_apply_of_ge`
`finSumNatEquiv_symm_apply_add_right` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumNatEquiv`	—	`finSumNatEquiv_symm_apply_of_ge`
`finSumNatEquiv_symm_apply_fin` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumNatEquiv`	—	`finSumNatEquiv_symm_apply_of_lt`
`finSumNatEquiv_symm_apply_of_ge` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumNatEquiv`	—	—
`finSumNatEquiv_symm_apply_of_lt` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumNatEquiv`	—	—
`finTwoArrowEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finTwoArrowEquiv` `Equiv.toFun` `piFinTwoEquiv`	—	—
`finTwoArrowEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finTwoArrowEquiv` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`isLeft_finSumNatEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumNatEquiv`	—	`finSumNatEquiv_symm_apply_of_lt` `finSumNatEquiv_symm_apply_of_ge` `LE.le.not_gt`
`isRight_finSumNatEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSumNatEquiv`	—	—
`prodEquivPiFinTwo_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodEquivPiFinTwo` `Fin.cons` `finZeroElim`	—	—
`prodEquivPiFinTwo_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `prodEquivPiFinTwo` `Fin.cons` `finZeroElim`	—	—

---

← Back to Index