haschu/nominal-lean.git/Algebra, branch main
Formalization of nominal sets in Lean 4.
https://git.haschu.me/haschu/nominal-lean.git/atom/Algebra?h=main
2026-04-15T13:17:13Z
move wip
2026-04-15T13:17:13Z
Hannes Schulze
contact@haschu.me
2026-04-15T13:17:13Z
urn:sha1:37f7c86a7591da1233cdf1d293bf851f43c65ba1
update lean
2026-04-15T11:22:40Z
Hannes Schulze
contact@haschu.me
2026-04-14T14:04:44Z
urn:sha1:a5ff8efe5b5e314e0aa759318e5fb194e066f612
Alg category
2025-12-05T22:51:59Z
Hannes Schulze
haschu0103@outlook.de
2025-12-05T22:51:59Z
urn:sha1:43942e78f4b3ed4cfca3b508f06161d0983c545e
revise OrbitFinite restriction for equations
2025-12-05T22:34:25Z
Hannes Schulze
haschu0103@outlook.de
2025-12-05T22:32:38Z
urn:sha1:7750ccdcb2afebe90da275f96e276a672a3c8a74
define algebras
2025-12-05T22:19:57Z
Hannes Schulze
haschu0103@outlook.de
2025-12-05T22:19:57Z
urn:sha1:aa280ca672aff145e811b79f4315ba200a09bad5
fix depth
2025-12-04T21:26:16Z
Hannes Schulze
haschu0103@outlook.de
2025-12-04T20:18:00Z
urn:sha1:cc3483496781b10b6acd2450117b443d03957dc4
prove that derivable equality is an equivariant equivalence
2025-12-04T18:05:06Z
Hannes Schulze
haschu0103@outlook.de
2025-12-04T18:05:06Z
urn:sha1:da3ddb5f61bb3dae9978770a26cf276c5265a1b8
implement derivable equality
2025-12-04T16:14:46Z
Hannes Schulze
haschu0103@outlook.de
2025-12-04T16:14:46Z
urn:sha1:8fdf459876b999dbe184196f9abd330a3c24d560
more cleanup
2025-12-03T20:52:56Z
Hannes Schulze
haschu0103@outlook.de
2025-12-03T20:45:09Z
urn:sha1:b00c95bd3580a8a8bd779f57a034900140ce41fa
differentiate bw substitution and uniform substitution
2025-12-03T20:22:03Z
Hannes Schulze
haschu0103@outlook.de
2025-12-03T20:22:03Z
urn:sha1:2edae587eee2ed64f66a4e4bedca6e654ad2f708