OAI/Topology/CoarseAssembly/FredholmModule.lean

Odd analytic Fredholm modules

These are the actual operator cycles for KK₁(A, ℂ): a separable Hilbert space, a star representation of A, and an operator whose commutator, self-adjointness defect and square defect are locally compact. We keep degenerate cycles, unitary equivalence, direct sum and norm homotopy explicit so that the analytic group can be formed as a quotient, rather than supplied as an arbitrary abelian group.