Quandle

📁 Source: Mathlib/Algebra/Quandle.lean

Statistics

Metric	Count
Definitions `Quandle`, `map`, `quandle`, `dihedralAct`, `instDihedral`, `oppositeQuandle`, `toRack`, `«term_→◃_»`, `«term_◃_»`, `«term_◃⁻¹_»`, `Rack`, `EnvelGroup`, `inhabited`, `IsAbelian`, `IsInvolutory`, `PreEnvelGroup`, `inhabited`, `setoid`, `PreEnvelGroupRel`, `PreEnvelGroupRel'`, `inhabited`, `act'`, `envelAction`, `instDivInvMonoidEnvelGroup`, `instGroupEnvelGroup`, `invAct`, `oppositeRack`, `selfApplyEquiv`, `toConj`, `toEnvelGroup`, `map`, `mapAux`, `toShelf`, `Shelf`, `act`, `ShelfHom`, `comp`, `id`, `inhabited`, `instFunLike`, `toFun`, `UnitalShelf`, `toOne`, `toShelf`	44
Theorems `conj_act_eq_conj`, `conj_swap`, `inv`, `fix`, `fix_inv`, `rel`, `refl`, `trans`, `act'_apply`, `act'_symm_apply`, `act_invAct_eq`, `ad_conj`, `assoc_iff_id`, `envelAction_prop`, `invAct_act_eq`, `invAct_apply`, `involutory_invAct_eq_act`, `left_cancel`, `left_cancel_inv`, `left_inv`, `op_act_op_eq`, `op_invAct_op_eq`, `right_inv`, `self_act_act_eq`, `self_act_eq_iff_eq`, `self_act_invAct_eq`, `self_distrib_inv`, `self_invAct_act_eq`, `self_invAct_eq_iff_eq`, `self_invAct_invAct_eq`, `well_def`, `univ`, `univ_uniq`, `self_distrib`, `comp_apply`, `ext`, `ext_iff`, `map_act`, `map_act'`, `toFun_eq_coe`, `act_act_self_eq`, `act_idem`, `act_one`, `act_self_act_eq`, `assoc`, `one_act`	46
Total	90

Quandle

Definitions

Name	Category	Theorems
`dihedralAct` 📖	CompOp	1 math math: `dihedralAct.inv`
`instDihedral` 📖	CompOp	—
`oppositeQuandle` 📖	CompOp	—
`toRack` 📖	CompOp	6 math math: `fix`, `Rack.envelAction_prop`, `conj_swap`, `Rack.toEnvelGroup.univ`, `conj_act_eq_conj`, `fix_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conj_act_eq_conj` 📖	mathematical	—	`Shelf.act` `Conj` `Rack.toShelf` `toRack` `Conj.quandle` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`conj_swap` 📖	mathematical	—	`Shelf.act` `Conj` `Rack.toShelf` `toRack` `Conj.quandle`	—	`eq_mul_inv_of_mul_eq` `inv_inv`
`fix` 📖	mathematical	—	`Shelf.act` `Rack.toShelf` `toRack`	—	—
`fix_inv` 📖	mathematical	—	`Rack.invAct` `toRack`	—	`Rack.left_cancel` `Rack.act_invAct_eq` `fix`

Quandle.Conj

Definitions

Name	Category	Theorems
`map` 📖	CompOp	1 math math: `Rack.toEnvelGroup.univ`
`quandle` 📖	CompOp	4 math math: `Rack.envelAction_prop`, `Quandle.conj_swap`, `Rack.toEnvelGroup.univ`, `Quandle.conj_act_eq_conj`

Quandle.dihedralAct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv` 📖	mathematical	—	`Function.Involutive` `ZMod` `Quandle.dihedralAct`	—	`sub_sub_cancel`

Quandles

Definitions

Name	Category	Theorems
`«term_→◃_»` 📖	CompOp	—
`«term_◃_»` 📖	CompOp	—
`«term_◃⁻¹_»` 📖	CompOp	—

Rack

Definitions

Name	Category	Theorems
`EnvelGroup` 📖	CompOp	2 math math: `envelAction_prop`, `toEnvelGroup.univ`
`IsAbelian` 📖	MathDef	—
`IsInvolutory` 📖	MathDef	—
`PreEnvelGroup` 📖	CompData	—
`PreEnvelGroupRel` 📖	CompData	2 math math: `PreEnvelGroupRel.refl`, `PreEnvelGroupRel'.rel`
`PreEnvelGroupRel'` 📖	CompData	—
`act'` 📖	CompOp	4 math math: `ad_conj`, `act'_apply`, `invAct_apply`, `act'_symm_apply`
`envelAction` 📖	CompOp	1 math math: `envelAction_prop`
`instDivInvMonoidEnvelGroup` 📖	CompOp	3 math math: `toEnvelGroup.univ_uniq`, `envelAction_prop`, `toEnvelGroup.univ`
`instGroupEnvelGroup` 📖	CompOp	2 math math: `envelAction_prop`, `toEnvelGroup.univ`
`invAct` 📖	CompOp	16 math math: `left_inv`, `right_inv`, `self_invAct_eq_iff_eq`, `left_cancel_inv`, `involutory_invAct_eq_act`, `act_invAct_eq`, `invAct_apply`, `self_distrib_inv`, `self_invAct_invAct_eq`, `invAct_act_eq`, `act'_symm_apply`, `op_act_op_eq`, `Quandle.fix_inv`, `self_invAct_act_eq`, `self_act_invAct_eq`, `op_invAct_op_eq`
`oppositeRack` 📖	CompOp	2 math math: `op_act_op_eq`, `op_invAct_op_eq`
`selfApplyEquiv` 📖	CompOp	—
`toConj` 📖	CompOp	—
`toEnvelGroup` 📖	CompOp	2 math math: `envelAction_prop`, `toEnvelGroup.univ`
`toShelf` 📖	CompOp	20 math math: `left_inv`, `right_inv`, `Quandle.fix`, `envelAction_prop`, `ad_conj`, `involutory_invAct_eq_act`, `Quandle.conj_swap`, `act_invAct_eq`, `act'_apply`, `toEnvelGroup.univ`, `left_cancel`, `Quandle.conj_act_eq_conj`, `assoc_iff_id`, `self_act_eq_iff_eq`, `self_act_act_eq`, `invAct_act_eq`, `op_act_op_eq`, `self_invAct_act_eq`, `self_act_invAct_eq`, `op_invAct_op_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`act'_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `act'` `Shelf.act` `toShelf`	—	—
`act'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `act'` `invAct`	—	—
`act_invAct_eq` 📖	mathematical	—	`Shelf.act` `toShelf` `invAct`	—	`right_inv`
`ad_conj` 📖	mathematical	—	`act'` `Shelf.act` `toShelf` `Equiv` `Equiv.Perm.instMul` `Equiv.Perm.instInv`	—	`eq_mul_inv_iff_mul_eq` `Equiv.Perm.ext` `Shelf.self_distrib`
`assoc_iff_id` 📖	mathematical	—	`Shelf.act` `toShelf`	—	`Shelf.self_distrib` `left_cancel`
`envelAction_prop` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `EnvelGroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `instDivInvMonoidEnvelGroup` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `envelAction` `ShelfHom` `Quandle.Conj` `toShelf` `Quandle.toRack` `Quandle.Conj.quandle` `instGroupEnvelGroup` `ShelfHom.instFunLike` `toEnvelGroup` `Shelf.act`	—	—
`invAct_act_eq` 📖	mathematical	—	`invAct` `Shelf.act` `toShelf`	—	`left_inv`
`invAct_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.Perm.instInv` `act'` `invAct`	—	—
`involutory_invAct_eq_act` 📖	mathematical	`IsInvolutory`	`invAct` `Shelf.act` `toShelf`	—	`left_cancel` `right_inv`
`left_cancel` 📖	mathematical	—	`Shelf.act` `toShelf`	—	`Equiv.injective`
`left_cancel_inv` 📖	mathematical	—	`invAct`	—	`Equiv.injective`
`left_inv` 📖	mathematical	—	`invAct` `Shelf.act` `toShelf`	—	—
`op_act_op_eq` 📖	mathematical	—	`Shelf.act` `MulOpposite` `toShelf` `oppositeRack` `MulOpposite.op` `invAct`	—	—
`op_invAct_op_eq` 📖	mathematical	—	`invAct` `MulOpposite` `oppositeRack` `MulOpposite.op` `Shelf.act` `toShelf`	—	—
`right_inv` 📖	mathematical	—	`invAct` `Shelf.act` `toShelf`	—	—
`self_act_act_eq` 📖	mathematical	—	`Shelf.act` `toShelf`	—	`right_inv` `Shelf.self_distrib`
`self_act_eq_iff_eq` 📖	mathematical	—	`Shelf.act` `toShelf`	—	`left_cancel` `right_inv` `self_act_act_eq`
`self_act_invAct_eq` 📖	mathematical	—	`invAct` `Shelf.act` `toShelf`	—	`left_cancel` `right_inv` `self_act_act_eq`
`self_distrib_inv` 📖	mathematical	—	`invAct`	—	`left_cancel` `right_inv` `Shelf.self_distrib`
`self_invAct_act_eq` 📖	mathematical	—	`Shelf.act` `toShelf` `invAct`	—	`self_act_invAct_eq`
`self_invAct_eq_iff_eq` 📖	mathematical	—	`invAct`	—	`self_act_eq_iff_eq`
`self_invAct_invAct_eq` 📖	mathematical	—	`invAct`	—	`self_act_act_eq`

Rack.EnvelGroup

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

Rack.PreEnvelGroup

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`setoid` 📖	CompOp	—

Rack.PreEnvelGroupRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`Rack.PreEnvelGroupRel`	—	—
`trans` 📖	—	`Rack.PreEnvelGroupRel`	—	—	`Rack.PreEnvelGroupRel'.rel`

Rack.PreEnvelGroupRel'

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rel` 📖	mathematical	—	`Rack.PreEnvelGroupRel`	—	—

Rack.toEnvelGroup

Definitions

Name	Category	Theorems
`map` 📖	CompOp	2 math math: `univ_uniq`, `univ`
`mapAux` 📖	CompOp	1 math math: `mapAux.well_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`univ` 📖	mathematical	—	`ShelfHom.comp` `Quandle.Conj` `Rack.EnvelGroup` `Rack.toShelf` `Quandle.toRack` `Quandle.Conj.quandle` `Rack.instGroupEnvelGroup` `Quandle.Conj.map` `DFunLike.coe` `Equiv` `ShelfHom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Rack.instDivInvMonoidEnvelGroup` `Group.toDivInvMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `map` `Rack.toEnvelGroup`	—	`Equiv.symm_apply_apply`
`univ_uniq` 📖	mathematical	`ShelfHom.comp` `Quandle.Conj` `Rack.EnvelGroup` `Rack.toShelf` `Quandle.toRack` `Quandle.Conj.quandle` `Rack.instGroupEnvelGroup` `Quandle.Conj.map` `Rack.toEnvelGroup`	`DFunLike.coe` `Equiv` `ShelfHom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Rack.instDivInvMonoidEnvelGroup` `Group.toDivInvMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `map`	—	`Equiv.apply_symm_apply`

Rack.toEnvelGroup.mapAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`well_def` 📖	mathematical	—	`Rack.toEnvelGroup.mapAux`	—	`mul_assoc` `one_mul` `mul_one` `inv_mul_cancel` `ShelfHom.map_act`

Shelf

Definitions

Name	Category	Theorems
`act` 📖	CompOp	28 math math: `self_distrib`, `Rack.left_inv`, `Rack.right_inv`, `Quandle.fix`, `Rack.envelAction_prop`, `Rack.ad_conj`, `UnitalShelf.one_act`, `Rack.involutory_invAct_eq_act`, `Quandle.conj_swap`, `Rack.act_invAct_eq`, `ShelfHom.map_act`, `ShelfHom.map_act'`, `Rack.act'_apply`, `UnitalShelf.act_one`, `UnitalShelf.act_self_act_eq`, `Rack.left_cancel`, `Quandle.conj_act_eq_conj`, `Rack.assoc_iff_id`, `Rack.self_act_eq_iff_eq`, `Rack.self_act_act_eq`, `Rack.invAct_act_eq`, `UnitalShelf.act_idem`, `Rack.op_act_op_eq`, `Rack.self_invAct_act_eq`, `Rack.self_act_invAct_eq`, `UnitalShelf.act_act_self_eq`, `UnitalShelf.assoc`, `Rack.op_invAct_op_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`self_distrib` 📖	mathematical	—	`act`	—	—

ShelfHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	2 math math: `Rack.toEnvelGroup.univ`, `comp_apply`
`id` 📖	CompOp	—
`inhabited` 📖	CompOp	—
`instFunLike` 📖	CompOp	4 math math: `Rack.envelAction_prop`, `map_act`, `comp_apply`, `toFun_eq_coe`
`toFun` 📖	CompOp	3 math math: `map_act'`, `ext_iff`, `toFun_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `ShelfHom` `instFunLike` `comp`	—	—
`ext` 📖	—	`toFun`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun`	—	`ext`
`map_act` 📖	mathematical	—	`DFunLike.coe` `ShelfHom` `instFunLike` `Shelf.act`	—	`map_act'`
`map_act'` 📖	mathematical	—	`toFun` `Shelf.act`	—	—
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `ShelfHom` `instFunLike`	—	—

UnitalShelf

Definitions

Name	Category	Theorems
`toOne` 📖	CompOp	2 math math: `one_act`, `act_one`
`toShelf` 📖	CompOp	6 math math: `one_act`, `act_one`, `act_self_act_eq`, `act_idem`, `act_act_self_eq`, `assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`act_act_self_eq` 📖	mathematical	—	`Shelf.act` `toShelf`	—	`act_one` `Shelf.self_distrib`
`act_idem` 📖	mathematical	—	`Shelf.act` `toShelf`	—	`act_one` `Shelf.self_distrib`
`act_one` 📖	mathematical	—	`Shelf.act` `toShelf` `toOne`	—	—
`act_self_act_eq` 📖	mathematical	—	`Shelf.act` `toShelf`	—	`act_one` `Shelf.self_distrib` `one_act`
`assoc` 📖	mathematical	—	`Shelf.act` `toShelf`	—	`Shelf.self_distrib` `act_act_self_eq` `act_self_act_eq`
`one_act` 📖	mathematical	—	`Shelf.act` `toShelf` `toOne`	—	—

(root)

Definitions

Name	Category	Theorems
`Quandle` 📖	CompData	—
`Rack` 📖	CompData	—
`Shelf` 📖	CompData	—
`ShelfHom` 📖	CompData	6 math math: `Rack.toEnvelGroup.univ_uniq`, `Rack.envelAction_prop`, `ShelfHom.map_act`, `Rack.toEnvelGroup.univ`, `ShelfHom.comp_apply`, `ShelfHom.toFun_eq_coe`
`UnitalShelf` 📖	CompData	—

---

← Back to Index