Commit 2023-01-26 13:48 e32b06c8

View on Github →

feat: Port Algebra.Quandle (#1817)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Quandle.lean

added def Quandle.Conj.map

added def Quandle.Conj

added def Quandle.Dihedral

added theorem Quandle.conj_act_eq_conj

added theorem Quandle.conj_swap

added theorem Quandle.dihedralAct.inv

added def Quandle.dihedralAct

added theorem Quandle.fix_inv

added def Rack.EnvelGroup

added def Rack.IsAbelian

added def Rack.IsInvolutory

added inductive Rack.PreEnvelGroup

added theorem Rack.PreEnvelGroupRel'.rel

added inductive Rack.PreEnvelGroupRel'

added theorem Rack.PreEnvelGroupRel.refl

added theorem Rack.PreEnvelGroupRel.symm

added theorem Rack.PreEnvelGroupRel.trans

added inductive Rack.PreEnvelGroupRel

added def Rack.act'

added theorem Rack.act'_apply

added theorem Rack.act'_symm_apply

added theorem Rack.act_invAct_eq

added theorem Rack.ad_conj

added theorem Rack.assoc_iff_id

added def Rack.envelAction

added theorem Rack.envelAction_prop

added theorem Rack.invAct_act_eq

added theorem Rack.invAct_apply

added theorem Rack.involutory_invAct_eq_act

added theorem Rack.left_cancel

added theorem Rack.left_cancel_inv

added theorem Rack.op_act_op_eq

added theorem Rack.op_invAct_op_eq

added def Rack.selfApplyEquiv

added theorem Rack.self_act_act_eq

added theorem Rack.self_act_eq_iff_eq

added theorem Rack.self_act_invAct_eq

added theorem Rack.self_distrib_inv

added theorem Rack.self_invAct_act_eq

added theorem Rack.self_invAct_eq_iff_eq

added theorem Rack.self_invAct_invAct_eq

added def Rack.toConj

added def Rack.toEnvelGroup.map

added theorem Rack.toEnvelGroup.mapAux.well_def

added def Rack.toEnvelGroup.mapAux

added theorem Rack.toEnvelGroup.univ

added theorem Rack.toEnvelGroup.univ_uniq

added def Rack.toEnvelGroup

added def ShelfHom.comp

added theorem ShelfHom.comp_apply

added def ShelfHom.id

added theorem ShelfHom.map_act

added structure ShelfHom