Commit 2023-11-02 21:53 78305a20

View on Github →

chore(LinearAlgebra): remove redundant [Nontrivial R] (#8129) These can be inferred from [StrictOrderedSemiring R].

Estimated changes

Modified Mathlib/LinearAlgebra/Orientation.lean

modified theorem Basis.abs_det_adjustToOrientation

modified def Basis.adjustToOrientation

modified theorem Basis.adjustToOrientation_apply_eq_or_eq_neg

modified theorem Basis.det_adjustToOrientation

modified theorem Basis.orientation_adjustToOrientation

modified theorem Basis.orientation_isEmpty

modified theorem Basis.orientation_map

modified theorem Basis.orientation_neg_single

modified theorem Basis.orientation_reindex

modified theorem Basis.orientation_unitsSMul

modified theorem Orientation.eq_or_eq_neg_of_isEmpty

modified theorem Orientation.map_positiveOrientation_of_isEmpty