haschu/nominal-lean.git/Nominal/Basic.lean, branch graded-algebraFormalization of nominal sets in Lean 4.https://git.haschu.me/haschu/nominal-lean.git/atom/Nominal/Basic.lean?h=graded-algebra2025-10-21T19:45:34Zrestructure2025-10-21T19:45:34ZHannes Schulzehaschu0103@outlook.de2025-10-21T19:45:34Zurn:sha1:e2bde40a31e0ab0fea7e412bd2f9b03edcc026ddvery rough draft for support_inter2025-10-21T18:41:37ZHannes Schulzehaschu0103@outlook.de2025-10-21T18:41:37Zurn:sha1:8514856d26803b8b36558fc226e51e8057c5d5e2simplify some more2025-10-21T09:38:28ZHannes Schulzehaschu0103@outlook.de2025-10-21T09:38:28Zurn:sha1:729a15c501ee42a7ed3a4b002d1366bde6406f92add some proofs about specific least supports2025-10-20T22:00:50ZHannes Schulzehaschu0103@outlook.de2025-10-20T22:00:50Zurn:sha1:0b7c12eb301fe701e92ac02e5f6e6f92a8ededecsome simplifications2025-10-20T20:26:30ZHannes Schulzehaschu0103@outlook.de2025-10-20T20:26:30Zurn:sha1:bb10205c22e4518f286ab59ad0e23b14756ec851prove things about intersections and supports2025-10-20T20:23:31ZHannes Schulzehaschu0103@outlook.de2025-10-20T20:23:31Zurn:sha1:0504bfded36c773cde9a252c1ee058e0bcfab6f0further work2025-10-20T11:13:33ZHannes Schulzehaschu0103@outlook.de2025-10-20T11:13:33Zurn:sha1:992aa8fdd40521d2cc7ed4759bce92c912cbeb80further work on nominal set definition2025-10-19T22:48:05ZHannes Schulzehaschu0103@outlook.de2025-10-19T22:48:05Zurn:sha1:d07d97f720f2bb2373fca0e96c906338d4d4631eimplement group of finitely supported permutations2025-09-25T20:43:39ZHannes Schulzehaschu0103@outlook.de2025-09-25T20:11:38Zurn:sha1:7a571004a8dd874d0af95cdc7f80fdf61f9c1c9finitial commit2025-09-19T11:03:48ZHannes Schulzehaschu0103@outlook.de2025-09-19T11:03:48Zurn:sha1:c92169d23ec70e453bf1b84c82b224997065e0ff