Commit 2024-11-23 08:16 84d03da2

feat(LinearAlgebra/QuadraticForm/Basic): weaken invertibility hypothesis on 2 (#14986) The aim of this is to eventually enable base-change of quadratic maps from a (not necessarily (torsion-)free) abelian group to an abelian group on which 2 is invertible (e.g., the real numbers). The current set-up requires 2 to be invertible in the base ring (which would be the integers in the situation above). This PR weakens the assumption for the definition of QuadraticMap.associatedHom and QuadraticMap.associated from [Invertible (2 : R)] to [Invertible (2 : Module.End R N)], where N is the target module of he quadratic map. See this discussion on Zulip. On the way, we fix some mistakes in docstrings.