Orientation

📁 Source: Mathlib/LinearAlgebra/Orientation.lean

Statistics

Metric	Count
Definitions oriented, adjustToOrientation, orientation, Oriented, positiveOrientation, Orientation, map, reindex, someBasis	9
Theorems abs_det_adjustToOrientation, adjustToOrientation_apply_eq_or_eq_neg, det_adjustToOrientation, map_orientation_eq_det_inv_smul, orientation_adjustToOrientation, orientation_comp_linearEquiv_eq_iff_det_pos, orientation_comp_linearEquiv_eq_neg_iff_det_neg, orientation_eq_iff_det_pos, orientation_eq_or_eq_neg, orientation_isEmpty, orientation_map, orientation_ne_iff_eq_neg, orientation_neg_single, orientation_reindex, orientation_unitsSMul, eq_or_eq_neg, eq_or_eq_neg_of_isEmpty, map_apply, map_eq_det_inv_smul, map_eq_iff_det_pos, map_eq_neg_iff_det_neg, map_neg, map_of_isEmpty, map_positiveOrientation_of_isEmpty, map_refl, map_symm, ne_iff_eq_neg, reindex_apply, reindex_neg, reindex_refl, reindex_symm, someBasis_orientation	32
Total	41

IsEmpty

Definitions

Name	Category	Theorems
oriented 📖	CompOp	5 math math: Orientation.volumeForm_zero_pos, Module.Basis.orientation_isEmpty, Orientation.volumeForm_zero_neg, Orientation.eq_or_eq_neg_of_isEmpty, Orientation.map_positiveOrientation_of_isEmpty

Module

Definitions

Name	Category	Theorems
Oriented 📖	CompData	—

Module.Basis

Definitions

Name	Category	Theorems
adjustToOrientation 📖	CompOp	6 math math: det_adjustToOrientation, OrthonormalBasis.toBasis_adjustToOrientation, orientation_adjustToOrientation, abs_det_adjustToOrientation, OrthonormalBasis.orthonormal_adjustToOrientation, adjustToOrientation_apply_eq_or_eq_neg
orientation 📖	CompOp	15 math math: orientation_eq_iff_det_pos, orientation_eq_or_eq_neg, orientation_ne_iff_eq_neg, orientation_comp_linearEquiv_eq_iff_det_pos, orientation_adjustToOrientation, orientation_comp_linearEquiv_eq_neg_iff_det_neg, orientation_isEmpty, Orientation.someBasis_orientation, orientation_unitsSMul, OrthonormalBasis.same_orientation_iff_det_eq_det, Orientation.finOrthonormalBasis_orientation, OrthonormalBasis.orientation_adjustToOrientation, orientation_neg_single, orientation_map, orientation_reindex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_det_adjustToOrientation 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det adjustToOrientation	—	det_adjustToOrientation abs_neg
adjustToOrientation_apply_eq_or_eq_neg 📖	mathematical	—	DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike adjustToOrientation NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	adjustToOrientation.eq_1 unitsSMul_apply Function.update_self Units.neg_smul one_smul Function.update_of_ne
det_adjustToOrientation 📖	mathematical	—	det adjustToOrientation AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instNeg Ring.toAddCommGroup CommRing.toRing	—	Algebra.to_smulCommClass det_unitsSMul Finset.prod_update_of_mem Finset.prod_congr Finset.prod_const_one mul_one inv_neg inv_one AlternatingMap.ext neg_smul one_smul
map_orientation_eq_det_inv_smul 📖	mathematical	—	DFunLike.coe Equiv Orientation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike Orientation.map Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction instMulActionRay AlternatingMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommMonoid AlternatingMap.instModule Units.instGroup Units.instDistribMulAction AddCommMonoid.toAddMonoid AlternatingMap.instDistribMulAction Module.toDistribMulAction NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id Units.smulCommClass_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AlternatingMap.instSMulCommClass Units.instInv MonoidHom LinearEquiv RingHom.id RingHomInvPair.ids MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det	—	RingHomInvPair.ids nonempty_fintype Algebra.to_smulCommClass Units.smulCommClass_right AlternatingMap.instSMulCommClass Module.Ray.ind AlternatingMap.compLinearEquiv_eq_zero_iff Orientation.map_apply smul_ne_zero_iff_ne smul_rayOfNeZero ray_eq_iff Units.smul_def AlternatingMap.eq_smul_basis_det AlternatingMap.compLinearMap_apply AlternatingMap.smul_apply det_comp det_self mul_one smul_eq_mul mul_comm SemigroupAction.mul_smul LinearEquiv.coe_inv_det SameRay.refl
orientation_adjustToOrientation 📖	mathematical	—	orientation SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder adjustToOrientation	—	adjustToOrientation.eq_1 orientation_neg_single orientation_ne_iff_eq_neg
orientation_comp_linearEquiv_eq_iff_det_pos 📖	mathematical	—	orientation SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder map CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids orientation_map Algebra.to_smulCommClass Units.smulCommClass_right AlternatingMap.instSMulCommClass map_orientation_eq_det_inv_smul Finite.of_fintype smulCommClass_self units_inv_smul units_smul_eq_self_iff AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE NoZeroDivisors.toNoZeroSMulDivisors IsStrictOrderedRing.noZeroDivisors LinearEquiv.coe_det
orientation_comp_linearEquiv_eq_neg_iff_det_neg 📖	mathematical	—	orientation SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder map CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Orientation instNegRay AlternatingMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup CommRing.toRing AlternatingMap.instModule Preorder.toLT PartialOrder.toPreorder DFunLike.coe MonoidHom LinearMap RingHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap RingHomInvPair.ids MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids orientation_map Algebra.to_smulCommClass Units.smulCommClass_right AlternatingMap.instSMulCommClass map_orientation_eq_det_inv_smul Finite.of_fintype smulCommClass_self units_inv_smul units_smul_eq_neg_iff AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE NoZeroDivisors.toNoZeroSMulDivisors IsStrictOrderedRing.noZeroDivisors LinearEquiv.coe_det
orientation_eq_iff_det_pos 📖	mathematical	—	orientation SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule AlternatingMap.instFunLike det Module.Basis instFunLike	—	Algebra.to_smulCommClass ray_eq_iff AlternatingMap.eq_smul_basis_det sameRay_smul_left_iff_of_ne AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE NoZeroDivisors.toNoZeroSMulDivisors IsStrictOrderedRing.noZeroDivisors det_ne_zero instNontrivialOfCharZero IsStrictOrderedRing.toCharZero IsUnit.ne_zero isUnit_det
orientation_eq_or_eq_neg 📖	mathematical	—	orientation SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Orientation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instNegRay AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup CommRing.toRing AlternatingMap.instModule	—	Module.Ray.ind orientation.eq_1 ray_eq_iff neg_ne_zero neg_rayOfNeZero Algebra.to_smulCommClass AlternatingMap.eq_smul_basis_det sameRay_neg_smul_left_iff_of_ne AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE NoZeroDivisors.toNoZeroSMulDivisors IsStrictOrderedRing.noZeroDivisors det_ne_zero instNontrivialOfCharZero IsStrictOrderedRing.toCharZero AlternatingMap.map_basis_ne_zero_iff Finite.of_fintype sameRay_smul_left_iff_of_ne lt_or_lt_iff_ne
orientation_isEmpty 📖	mathematical	—	orientation Module.Oriented.positiveOrientation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid IsEmpty.oriented	—	orientation.eq_1 det_isEmpty
orientation_map 📖	mathematical	—	orientation map CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe Equiv Orientation EquivLike.toFunLike Equiv.instEquivLike Orientation.map	—	RingHomInvPair.ids AlternatingMap.compLinearEquiv_eq_zero_iff det_map' rayOfNeZero.congr_simp
orientation_ne_iff_eq_neg 📖	mathematical	—	Orientation CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid instNegRay AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup CommRing.toRing AlternatingMap.instModule orientation	—	orientation_eq_or_eq_neg Module.Ray.ne_neg_self IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors NoZeroDivisors.toNoZeroSMulDivisors IsStrictOrderedRing.noZeroDivisors
orientation_neg_single 📖	mathematical	—	orientation SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder unitsSMul CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Function.update Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Pi.instOne Units.instOne Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Orientation instNegRay AlternatingMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup CommRing.toRing AlternatingMap.instModule	—	Algebra.to_smulCommClass Units.smulCommClass_right AlternatingMap.instSMulCommClass orientation_unitsSMul Finset.prod_update_of_mem Finset.mem_univ Finset.prod_congr Finset.prod_const_one mul_one inv_neg inv_one AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE NoZeroDivisors.toNoZeroSMulDivisors IsStrictOrderedRing.noZeroDivisors IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
orientation_reindex 📖	mathematical	—	orientation reindex CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe Equiv Orientation EquivLike.toFunLike Equiv.instEquivLike Orientation.reindex	—	AlternatingMap.domDomCongr_eq_zero_iff det_reindex' rayOfNeZero.congr_simp
orientation_unitsSMul 📖	mathematical	—	orientation unitsSMul CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Orientation SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction instMulActionRay AlternatingMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommMonoid AlternatingMap.instModule Units.instGroup Units.instDistribMulAction AddCommMonoid.toAddMonoid AlternatingMap.instDistribMulAction Module.toDistribMulAction NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id Units.smulCommClass_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AlternatingMap.instSMulCommClass Units.instInv Finset.prod CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid Finset.univ	—	Algebra.to_smulCommClass Units.smulCommClass_right AlternatingMap.instSMulCommClass orientation.eq_1 smul_ne_zero_iff_ne smul_rayOfNeZero ray_eq_iff AlternatingMap.eq_smul_basis_det det_unitsSMul_self Units.smul_def smul_smul SameRay.congr_simp inv_mul_cancel one_smul SameRay.rfl

Module.Oriented

Definitions

Name	Category	Theorems
positiveOrientation 📖	CompOp	5 math math: Orientation.volumeForm_zero_pos, Module.Basis.orientation_isEmpty, Orientation.volumeForm_zero_neg, Orientation.eq_or_eq_neg_of_isEmpty, Orientation.map_positiveOrientation_of_isEmpty

Orientation

Definitions

Name	Category	Theorems
map 📖	CompOp	18 math math: map_symm, map_of_isEmpty, volumeForm_map, map_eq_neg_iff_det_neg, map_eq_iff_det_pos, rotation_map, map_eq_det_inv_smul, rightAngleRotation_map', map_neg, oangle_map, Module.Basis.map_orientation_eq_det_inv_smul, kahler_map, areaForm_map, map_refl, rightAngleRotation_map, map_apply, Module.Basis.orientation_map, map_positiveOrientation_of_isEmpty
reindex 📖	CompOp	5 math math: reindex_neg, reindex_refl, reindex_apply, reindex_symm, Module.Basis.orientation_reindex
someBasis 📖	CompOp	1 math math: someBasis_orientation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_or_eq_neg 📖	mathematical	Fintype.card Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Orientation Semifield.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instNegRay EuclideanDomain.toCommRing Field.toEuclideanDomain AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AlternatingMap.instModule	—	commRing_strongRankCondition EuclideanDomain.toNontrivial Module.Free.of_divisionRing Module.Basis.orientation_eq_or_eq_neg neg_neg
eq_or_eq_neg_of_isEmpty 📖	mathematical	—	Module.Oriented.positiveOrientation CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid IsEmpty.oriented Orientation instNegRay AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup CommRing.toRing AlternatingMap.instModule	—	Module.Ray.ind neg_ne_zero sameRay_or_sameRay_neg_iff_not_linearIndependent AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE NoZeroDivisors.toNoZeroSMulDivisors IsStrictOrderedRing.noZeroDivisors RingHomInvPair.ids Algebra.to_smulCommClass smulCommClass_self Fintype.complete Matrix.cons_val_fin_one LinearIndependent.map' LinearEquiv.ker NeZero.charZero_one IsStrictOrderedRing.toCharZero linearIndependent_iff' Finset.sum_congr Fin.sum_univ_succ one_mul Finset.univ_unique Matrix.cons_val_succ mul_one Finset.sum_neg_distrib Finset.sum_const Finset.card_singleton one_smul add_neg_cancel
map_apply 📖	mathematical	—	DFunLike.coe Equiv Orientation EquivLike.toFunLike Equiv.instEquivLike map rayOfNeZero AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommMonoid AlternatingMap.instModule AlternatingMap.compLinearMap LinearEquiv.toLinearMap RingHom.id RingHomInvPair.ids LinearEquiv.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AlternatingMap.instZero AlternatingMap.compLinearEquiv_eq_zero_iff	—	RingHomInvPair.ids
map_eq_det_inv_smul 📖	mathematical	Fintype.card Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe Equiv Orientation Semifield.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder EquivLike.toFunLike Equiv.instEquivLike map Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction instMulActionRay AlternatingMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommMonoid AlternatingMap.instModule Units.instGroup Units.instDistribMulAction AddCommMonoid.toAddMonoid AlternatingMap.instDistribMulAction Module.toDistribMulAction NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id Units.smulCommClass_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AlternatingMap.instSMulCommClass Units.instInv MonoidHom LinearEquiv RingHom.id RingHomInvPair.ids MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det	—	RingHomInvPair.ids Module.Basis.map_orientation_eq_det_inv_smul Finite.of_fintype commRing_strongRankCondition EuclideanDomain.toNontrivial Module.Free.of_divisionRing
map_eq_iff_det_pos 📖	mathematical	Fintype.card Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe Equiv Orientation Semifield.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder EquivLike.toFunLike Equiv.instEquivLike map Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids isEmpty_or_nonempty Fintype.card_eq_zero map_of_isEmpty LinearMap.det_eq_one_of_finrank_eq_zero IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Algebra.to_smulCommClass Units.smulCommClass_right AlternatingMap.instSMulCommClass map_eq_det_inv_smul smulCommClass_self units_inv_smul units_smul_eq_self_iff AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors LinearEquiv.coe_det
map_eq_neg_iff_det_neg 📖	mathematical	Fintype.card Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe Equiv Orientation Semifield.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder EquivLike.toFunLike Equiv.instEquivLike map instNegRay EuclideanDomain.toCommRing Field.toEuclideanDomain AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AlternatingMap.instModule Preorder.toLT PartialOrder.toPreorder MonoidHom LinearMap CommRing.toCommSemiring RingHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap RingHomInvPair.ids MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids isEmpty_or_nonempty Fintype.card_eq_zero map_of_isEmpty Module.Ray.ne_neg_self instIsDomain AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LinearMap.det_eq_one_of_finrank_eq_zero IsStrictOrderedRing.toZeroLEOneClass Fintype.card_pos Algebra.to_smulCommClass Units.smulCommClass_right AlternatingMap.instSMulCommClass map_eq_det_inv_smul FiniteDimensional.of_finrank_pos smulCommClass_self units_inv_smul units_smul_eq_neg_iff LinearEquiv.coe_det
map_neg 📖	mathematical	—	DFunLike.coe Equiv Orientation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike map instNegRay AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup CommRing.toRing AlternatingMap.instModule	—	RingHomInvPair.ids Module.Ray.map_neg
map_of_isEmpty 📖	mathematical	—	DFunLike.coe Equiv Orientation EquivLike.toFunLike Equiv.instEquivLike map	—	RingHomInvPair.ids Module.Ray.ind AlternatingMap.compLinearEquiv_eq_zero_iff map_apply AlternatingMap.ext AlternatingMap.compLinearMap_apply Unique.instSubsingleton
map_positiveOrientation_of_isEmpty 📖	mathematical	—	DFunLike.coe Equiv Orientation EquivLike.toFunLike Equiv.instEquivLike map Module.Oriented.positiveOrientation IsEmpty.oriented	—	RingHomInvPair.ids
map_refl 📖	mathematical	—	map LinearEquiv.refl CommSemiring.toSemiring Equiv.refl Orientation	—	map.eq_1 RingHomInvPair.ids AlternatingMap.domLCongr_refl Module.Ray.map_refl
map_symm 📖	mathematical	—	Equiv.symm Orientation map LinearEquiv.symm CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids	—	RingHomInvPair.ids
ne_iff_eq_neg 📖	mathematical	Fintype.card Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Orientation Semifield.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instNegRay EuclideanDomain.toCommRing Field.toEuclideanDomain AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AlternatingMap.instModule	—	eq_or_eq_neg Module.Ray.ne_neg_self instIsDomain AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
reindex_apply 📖	mathematical	—	DFunLike.coe Equiv Orientation EquivLike.toFunLike Equiv.instEquivLike reindex rayOfNeZero AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommMonoid AlternatingMap.instModule AlternatingMap.domDomCongr AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AlternatingMap.instZero AlternatingMap.domDomCongr_eq_zero_iff	—	—
reindex_neg 📖	mathematical	—	DFunLike.coe Equiv Orientation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike reindex instNegRay AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Ring.toAddCommGroup CommRing.toRing AlternatingMap.instModule	—	Module.Ray.map_neg
reindex_refl 📖	mathematical	—	reindex Equiv.refl Orientation	—	reindex.eq_1 RingHomInvPair.ids AlternatingMap.domDomCongrₗ_refl Module.Ray.map_refl
reindex_symm 📖	mathematical	—	Equiv.symm Orientation reindex	—	—
someBasis_orientation 📖	mathematical	Fintype.card Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Module.Basis.orientation EuclideanDomain.toCommRing Field.toEuclideanDomain SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder someBasis	—	Module.Basis.orientation_adjustToOrientation

(root)

Definitions

Name	Category	Theorems
Orientation 📖	CompOp	39 math math: Orientation.ne_iff_eq_neg, Orientation.volumeForm_neg_orientation, Orientation.map_symm, Orientation.eq_or_eq_neg, Orientation.map_of_isEmpty, Orientation.volumeForm_map, Orientation.map_eq_neg_iff_det_neg, Orientation.areaForm_neg_orientation, Orientation.reindex_neg, Orientation.map_eq_iff_det_pos, Orientation.reindex_refl, Orientation.rotation_map, Module.Basis.orientation_eq_or_eq_neg, Orientation.kahler_neg_orientation, Orientation.map_eq_det_inv_smul, Orientation.rightAngleRotation_map', Module.Basis.orientation_ne_iff_eq_neg, Orientation.rotation_neg_orientation_eq_neg, Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg, Orientation.map_neg, Orientation.oangle_map, Module.Basis.map_orientation_eq_det_inv_smul, Orientation.rightAngleRotation_trans_neg_orientation, Orientation.kahler_map, Orientation.volumeForm_zero_neg, Orientation.areaForm_map, Module.Basis.orientation_unitsSMul, Orientation.reindex_apply, Orientation.map_refl, Orientation.rightAngleRotation_map, Orientation.map_apply, Module.Basis.orientation_neg_single, Orientation.eq_or_eq_neg_of_isEmpty, Orientation.oangle_neg_orientation_eq_neg, Module.Basis.orientation_map, Orientation.reindex_symm, Orientation.map_positiveOrientation_of_isEmpty, Orientation.rightAngleRotation_neg_orientation, Module.Basis.orientation_reindex

---

← Back to Index