Commit 2026-09-30 06:36 728a93ee

chore(Basic): move FunLike from Data (#43253) and an assorted set of about 50 files to Algebra and Order too. Generated by Claude Sonnet following the various README files, reviewed by myself. To Basic/

• {Data → Basic}/FunLike/Basic
• {Data → Basic}/FunLike/Embedding
• {Data → Basic}/FunLike/Equiv
• {Data → Basic}/SetLike/Basic
• {Data → Basic}/SProd
• {Data → Basic}/Opposite To Algebra/
• {Data/FunLike → Algebra/Group}/IsApply
• Data/FunLike/Group → Algebra/Group/FunLike
• Data/FunLike/Module → Algebra/Module/FunLike
• Data/FunLike/Ring → Algebra/Ring/FunLike
• Data/FunLike/Graded → Algebra/GradedFunLike
• {Data → Algebra/Notation}/Bracket
• Data/Int/AbsoluteValue → Algebra/Order/AbsoluteValue/Int
• Data/Int/Star → Algebra/Order/Star/Int
• Data/Rat/Star → Algebra/Order/Star/Rat
• Data/Multiset/OrderedMonoid → Algebra/Order/Monoid/Multiset To Order/
• Data/Set/Order → Order/Monotone/Set/Basic
• Data/Set/Monotone → Order/Monotone/Set/Congr
• Data/Set/Pairwise/Chain → Order/Preorder/PairwiseChain
• {Data → Order}/Setoid/Basic
• {Data → Order}/Setoid/Partition
• {Data → Order}/Setoid/Partition/Card
• {Data → Order}/Sigma/Lex
• Data/Sigma/Order → Order/Sigma
• Data/PSigma/Order → Order/PSigma
• Data/Prod/Lex → Order/Prod/Lex/Basic
• {Data → Order}/Sum/Order
• {Data → Order}/Sum/Lattice
• Data/Sym/Sym2/Order → Order/Sym2
• Data/Fin/SuccPredOrder → Order/SuccPred/Fin
• Data/Nat/SuccPred → Order/SuccPred/Nat
• Data/Int/SuccPred → Order/SuccPred/Int
• Data/PNat/Order → Order/SuccPred/PNat
• Data/ENat/SuccOrder → Order/SuccPred/ENat
• {Data → Order}/Int/LeastGreatest
• {Data → Order}/Int/ConditionallyCompleteOrder To Logic/
• {Data → Logic}/PEquiv Assisted-by: Claude Sonnet 5