haschu/nominal-lean.git/Nominal/Instances/Basic.lean, branch graded-algebra
Formalization of nominal sets in Lean 4.
https://git.haschu.me/haschu/nominal-lean.git/atom/Nominal/Instances/Basic.lean?h=graded-algebra
2026-04-15T11:22:40Z
update lean
2026-04-15T11:22:40Z
Hannes Schulze
contact@haschu.me
2026-04-14T14:04:44Z
urn:sha1:a5ff8efe5b5e314e0aa759318e5fb194e066f612
define algebras
2025-12-05T22:19:57Z
Hannes Schulze
haschu0103@outlook.de
2025-12-05T22:19:57Z
urn:sha1:aa280ca672aff145e811b79f4315ba200a09bad5
implement derivable equality
2025-12-04T16:14:46Z
Hannes Schulze
haschu0103@outlook.de
2025-12-04T16:14:46Z
urn:sha1:8fdf459876b999dbe184196f9abd330a3c24d560
refactor equivariant props to use type classes
2025-12-03T19:34:41Z
Hannes Schulze
haschu0103@outlook.de
2025-12-03T19:34:41Z
urn:sha1:71a6a3d5b6f4b428b463bc4a0766c91d8c1d5768
minor cleanup
2025-12-02T10:52:55Z
Hannes Schulze
haschu0103@outlook.de
2025-12-02T10:52:15Z
urn:sha1:a8915795c109980285e11ed53d453987c0917069
wip terms
2025-11-20T10:56:18Z
Hannes Schulze
haschu0103@outlook.de
2025-11-20T10:56:18Z
urn:sha1:ea38ef0cb2c57e10696c7fb6108732a6f454818c
refactor equivariance namespaces
2025-10-28T23:40:13Z
Hannes Schulze
haschu0103@outlook.de
2025-10-28T23:40:13Z
urn:sha1:5dde77b6db9fc78094363f91e0c6643a84be513e
quotient types as nominal sets
2025-10-27T20:58:56Z
Hannes Schulze
haschu0103@outlook.de
2025-10-27T20:58:56Z
urn:sha1:b3f26f306945ec9e391140f1645012ba11decb40
simplify FPerm computations
2025-10-25T23:20:20Z
Hannes Schulze
haschu0103@outlook.de
2025-10-25T23:19:45Z
urn:sha1:10edba2c0365a6858a74da22042c98f9d5fa1acc
use simp only everywhere except for last goal
2025-10-24T16:20:43Z
Hannes Schulze
haschu0103@outlook.de
2025-10-24T16:20:43Z
urn:sha1:6df3f662f0f23e837b70ef1f4a8b8dde4a7aa521