Commit 2023-12-13 00:39 681a4da8

feat: homomorphisms are linear over Z/nZ scalars (#8965) Port from PFR for using linear algebra on C_2^n, following the convention of AddMonoidHom.to{Int,Nat,Rat}LinearMap but in a different file to avoid circular import. For a separate PR:

@[reducible]
def module (h : ∀ (x : M), n • x = 0) : Module (ZMod n) M