Orientation

📁 Source: Mathlib/Analysis/InnerProductSpace/Orientation.lean

Statistics

Metric	Count
Definitions finOrthonormalBasis, volumeForm, adjustToOrientation	3
Theorems abs_volumeForm_apply_le, abs_volumeForm_apply_of_orthonormal, abs_volumeForm_apply_of_pairwise_orthogonal, finOrthonormalBasis_orientation, volumeForm_apply_le, volumeForm_comp_linearIsometryEquiv, volumeForm_def, volumeForm_map, volumeForm_neg_orientation, volumeForm_robust, volumeForm_robust', volumeForm_robust_neg, volumeForm_zero_neg, volumeForm_zero_pos, abs_det_adjustToOrientation, adjustToOrientation_apply_eq_or_eq_neg, det_adjustToOrientation, det_eq_neg_det_of_opposite_orientation, det_to_matrix_orthonormalBasis_of_opposite_orientation, det_to_matrix_orthonormalBasis_of_same_orientation, orientation_adjustToOrientation, orthonormal_adjustToOrientation, same_orientation_iff_det_eq_det, toBasis_adjustToOrientation	24
Total	27

Orientation

Definitions

Name	Category	Theorems
finOrthonormalBasis 📖	CompOp	2 math math: volumeForm_def, finOrthonormalBasis_orientation
volumeForm 📖	CompOp	16 math math: volumeForm_robust_neg, volumeForm_neg_orientation, volumeForm_map, abs_volumeForm_apply_of_orthonormal, areaForm_to_volumeForm, volumeForm_def, volumeForm_zero_pos, volumeForm_robust, measure_eq_volume, abs_volumeForm_apply_of_pairwise_orthogonal, volumeForm_robust', volumeForm_zero_neg, volumeForm_apply_le, volumeForm_comp_linearIsometryEquiv, measure_orthonormalBasis, abs_volumeForm_apply_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_volumeForm_apply_le 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup DFunLike.coe AlternatingMap Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instFunLike volumeForm Finset.prod Real.instCommMonoid Finset.univ Fin.fintype Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Fin.isEmpty' eq_or_eq_neg_of_isEmpty volumeForm_zero_pos abs_one Real.instIsOrderedRing Finset.prod_congr Finset.univ_eq_empty volumeForm_neg_orientation abs_neg Fintype.card_fin Fact.out IsWellOrder.toIsWellFounded Fin.Lt.isWellOrder FiniteDimensional.of_fact_finrank_eq_succ InnerProductSpace.gramSchmidtOrthonormalBasis_det volumeForm_robust' Finset.abs_prod Finset.prod_le_prod Real.instZeroLEOneClass IsOrderedRing.toPosMulMono abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add OrthonormalBasis.orthonormal one_mul abs_real_inner_le_norm
abs_volumeForm_apply_of_orthonormal 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup DFunLike.coe AlternatingMap Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instFunLike volumeForm OrthonormalBasis Fin.fintype OrthonormalBasis.instFunLike Real.instOne	—	Real.instIsStrictOrderedRing volumeForm_robust' abs_one Real.instIsOrderedRing Module.Basis.det_self
abs_volumeForm_apply_of_pairwise_orthogonal 📖	mathematical	Pairwise Real Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero	abs Real.lattice Real.instAddGroup DFunLike.coe AlternatingMap Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instFunLike volumeForm Finset.prod Real.instCommMonoid Finset.univ Fin.fintype Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Fin.isEmpty' eq_or_eq_neg_of_isEmpty volumeForm_zero_pos abs_one Real.instIsOrderedRing Finset.prod_congr Finset.univ_eq_empty volumeForm_neg_orientation abs_neg Fintype.card_fin Fact.out IsWellOrder.toIsWellFounded Fin.Lt.isWellOrder FiniteDimensional.of_fact_finrank_eq_succ InnerProductSpace.gramSchmidtOrthonormalBasis_det volumeForm_robust' Finset.abs_prod Finset.prod_eq_zero Finset.mem_univ inner_zero_right abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_zero InnerProductSpace.gramSchmidtOrthonormalBasis_apply_of_orthogonal inner_smul_left real_inner_self_eq_norm_mul_norm abs_of_nonneg mul_nonneg IsOrderedRing.toPosMulMono inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono norm_nonneg Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf
finOrthonormalBasis_orientation 📖	mathematical	Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	Module.Basis.orientation Real.commRing Real.partialOrder Real.instIsStrictOrderedRing SeminormedAddCommGroup.toAddCommGroup DenselyNormedField.toNormedField RCLike.toDenselyNormedField Fin.fintype OrthonormalBasis.toBasis finOrthonormalBasis	—	Real.instIsStrictOrderedRing OrthonormalBasis.orientation_adjustToOrientation FiniteDimensional.of_finrank_pos
volumeForm_apply_le 📖	mathematical	—	Real Real.instLE DFunLike.coe AlternatingMap Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instFunLike volumeForm Finset.prod Real.instCommMonoid Finset.univ Fin.fintype Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing LE.le.trans le_abs_self abs_volumeForm_apply_le
volumeForm_comp_linearIsometryEquiv 📖	mathematical	Real Real.instLT Real.instZero DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap Real.semiring RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv	AlternatingMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instFunLike volumeForm LinearIsometryEquiv EquivLike.toFunLike LinearIsometryEquiv.instEquivLike	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Fin.isEmpty' eq_or_eq_neg_of_isEmpty volumeForm_zero_pos volumeForm_neg_orientation FiniteDimensional.of_fact_finrank_eq_succ map_eq_iff_det_pos Fact.out Fintype.card_fin LinearIsometryEquiv.symm_apply_apply volumeForm_map
volumeForm_def 📖	mathematical	—	volumeForm Module.Basis.det Real Real.commRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace Fin.fintype OrthonormalBasis.toBasis finOrthonormalBasis	—	Real.instIsStrictOrderedRing Fin.isEmpty'
volumeForm_map 📖	mathematical	—	DFunLike.coe AlternatingMap Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instFunLike volumeForm Equiv Orientation Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearIsometryEquiv LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Fin.isEmpty' eq_or_eq_neg_of_isEmpty volumeForm_zero_pos volumeForm.congr_simp map_neg volumeForm_neg_orientation Fact.out finOrthonormalBasis_orientation Module.Basis.orientation_map volumeForm_robust Module.Basis.det_map
volumeForm_neg_orientation 📖	mathematical	—	volumeForm Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instNegRay Real.commRing AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Real.instAddCommGroup AlternatingMap.instModule Real.semiring Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instNeg SeminormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing Fin.isEmpty' eq_or_eq_neg_of_isEmpty volumeForm_zero_neg volumeForm_zero_pos RingHomInvPair.ids smulCommClass_self volumeForm.congr_simp neg_neg Fact.out finOrthonormalBasis_orientation Module.Basis.orientation_ne_iff_eq_neg volumeForm_robust volumeForm_robust_neg
volumeForm_robust 📖	mathematical	Module.Basis.orientation Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace Fin.fintype OrthonormalBasis.toBasis	volumeForm Module.Basis.det	—	Real.instIsStrictOrderedRing Fin.isEmpty' Module.Basis.orientation_isEmpty volumeForm_def Module.Basis.det_isEmpty OrthonormalBasis.same_orientation_iff_det_eq_det finOrthonormalBasis_orientation
volumeForm_robust' 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup DFunLike.coe AlternatingMap Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instFunLike volumeForm CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Module.Basis.det Fin.fintype OrthonormalBasis.toBasis	—	Real.instIsStrictOrderedRing Fin.isEmpty' eq_or_eq_neg_of_isEmpty volumeForm_zero_pos abs_one Real.instIsOrderedRing Module.Basis.det_isEmpty volumeForm_neg_orientation abs_neg volumeForm_robust OrthonormalBasis.orientation_adjustToOrientation OrthonormalBasis.abs_det_adjustToOrientation
volumeForm_robust_neg 📖	mathematical	—	volumeForm AlternatingMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instNeg Real.instAddCommGroup Module.Basis.det Fin.fintype OrthonormalBasis.toBasis	—	Real.instIsStrictOrderedRing Fin.isEmpty' Module.Basis.orientation_isEmpty volumeForm_def Module.Basis.det_isEmpty Fact.out OrthonormalBasis.det_eq_neg_det_of_opposite_orientation finOrthonormalBasis_orientation
volumeForm_zero_neg 📖	mathematical	—	volumeForm Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instNegRay Real.commRing AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Real.instAddCommGroup AlternatingMap.instModule Module.Oriented.positiveOrientation IsEmpty.oriented Fin.isEmpty' Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instNeg SeminormedAddCommGroup.toAddCommGroup DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids AlternatingMap.instAddCommMonoid smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv AlternatingMap.constLinearEquivOfIsEmpty Real.instOne	—	Real.instIsStrictOrderedRing Fin.isEmpty' RingHomInvPair.ids smulCommClass_self volumeForm_def neg_ne_zero ray_eq_iff SameRay.sameRay_comm Matrix.zero_empty NeZero.charZero_one RCLike.charZero_rclike eq_zero_of_sameRay_self_neg Real.instIsDomain AlternatingMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
volumeForm_zero_pos 📖	mathematical	—	volumeForm Module.Oriented.positiveOrientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike IsEmpty.oriented Fin.isEmpty' DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal AlternatingMap.instAddCommMonoid AlternatingMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv AlternatingMap.constLinearEquivOfIsEmpty Real.instOne	—	Real.instIsStrictOrderedRing Fin.isEmpty' volumeForm_def

OrthonormalBasis

Definitions

Name	Category	Theorems
adjustToOrientation 📖	CompOp	5 math math: toBasis_adjustToOrientation, det_adjustToOrientation, adjustToOrientation_apply_eq_or_eq_neg, orientation_adjustToOrientation, abs_det_adjustToOrientation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_det_adjustToOrientation 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det toBasis adjustToOrientation	—	Real.instIsStrictOrderedRing toBasis_adjustToOrientation Module.Basis.abs_det_adjustToOrientation
adjustToOrientation_apply_eq_or_eq_neg 📖	mathematical	—	DFunLike.coe OrthonormalBasis Real Real.instRCLike instFunLike adjustToOrientation NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing toBasis_adjustToOrientation Module.Basis.adjustToOrientation_apply_eq_or_eq_neg
det_adjustToOrientation 📖	mathematical	—	Module.Basis.det Real Real.commRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace toBasis adjustToOrientation AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instNeg Real.instAddCommGroup	—	Real.instIsStrictOrderedRing Module.Basis.det_adjustToOrientation
det_eq_neg_det_of_opposite_orientation 📖	mathematical	—	Module.Basis.det Real Real.commRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace toBasis AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instNeg Real.instAddCommGroup	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass AlternatingMap.eq_smul_basis_det det_to_matrix_orthonormalBasis_of_opposite_orientation neg_smul one_smul
det_to_matrix_orthonormalBasis_of_opposite_orientation 📖	mathematical	—	DFunLike.coe AlternatingMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det toBasis OrthonormalBasis instFunLike Real.instNeg Real.instOne	—	Real.instIsStrictOrderedRing Mathlib.Tactic.Contrapose.contrapose₂ Module.Basis.orientation_eq_iff_det_pos det_to_matrix_orthonormalBasis_real Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
det_to_matrix_orthonormalBasis_of_same_orientation 📖	mathematical	Module.Basis.orientation Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace toBasis	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det OrthonormalBasis instFunLike Real.instOne	—	Real.instIsStrictOrderedRing det_to_matrix_orthonormalBasis_real Module.Basis.orientation_eq_iff_det_pos Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq
orientation_adjustToOrientation 📖	mathematical	—	Module.Basis.orientation Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace toBasis adjustToOrientation	—	Real.instIsStrictOrderedRing toBasis_adjustToOrientation Module.Basis.orientation_adjustToOrientation
orthonormal_adjustToOrientation 📖	mathematical	—	Orthonormal Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Module.Basis.instFunLike Module.Basis.adjustToOrientation Real.linearOrder Real.instIsStrictOrderedRing toBasis	—	Real.instIsStrictOrderedRing Orthonormal.orthonormal_of_forall_eq_or_eq_neg orthonormal Module.Basis.adjustToOrientation_apply_eq_or_eq_neg
same_orientation_iff_det_eq_det 📖	mathematical	—	Module.Basis.det Real Real.commRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace toBasis Module.Basis.orientation Real.partialOrder Real.instIsStrictOrderedRing	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass AlternatingMap.eq_smul_basis_det det_to_matrix_orthonormalBasis_of_same_orientation one_smul
toBasis_adjustToOrientation 📖	mathematical	—	toBasis Real Real.instRCLike adjustToOrientation Module.Basis.adjustToOrientation Real.commRing Real.linearOrder Real.instIsStrictOrderedRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace	—	Real.instIsStrictOrderedRing Module.Basis.toBasis_toOrthonormalBasis orthonormal_adjustToOrientation

---

← Back to Index