Mem iff transpose mul minkowski Matrix mul self

lemma mem_iff_transpose_mul_minkowskiMatrix_mul_self    (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :    Λ ∈ LorentzGroup d ↔ Λᵀ * η * Λ = η := by  rw [mem_iff_dual_mul_self]  rw [dual]  constructor  · intro h    have h' : η * ((η * Λᵀ * η) * Λ) = η * 1 := congr_arg (η * ·) h    rw [mul_one] at h'    simp_rw [← mul_assoc, sq, one_mul] at h'    exact h'  · intro h    calc      (η * Λᵀ * η) * Λ = η * (Λᵀ * η * Λ) := by simp_rw [mul_assoc]      _ = η * η := by rw [h]      _ = 1 := by rw [minkowskiMatrix.sq]