Determinant of a module reflection

This file computes the determinant of Mathlib's Module.reflection on a finite free module.

@[simp]

theorem Module.det_reflection {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (h : f x = 2) [Free R M] [Module.Finite R M] : LinearEquiv.det (reflection h) = -1

The determinant of a module reflection is -1 on a finite free module.