CrossProduct

📁 Source: Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_ofLp_crossProduct, norm_toLp_symm_crossProduct	2
Total	2

InnerProductGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_ofLp_crossProduct 📖	mathematical	—	Norm.norm WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.instNorm Real Fin.fintype Real.norm WithLp.toLp DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id crossProduct WithLp.ofLp Real.instMul EuclideanSpace Real.sin angle PiLp.normedAddCommGroup fact_one_le_two_ennreal Real.normedAddCommGroup PiLp.innerProductSpace Real.instRCLike RCLike.toInnerProductSpaceReal	—	fact_one_le_two_ennreal sin_angle_nonneg Nat.instAtLeastTwoHAddOfNat Function.smulCommClass Algebra.to_smulCommClass sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg mul_nonneg IsOrderedRing.toPosMulMono InnerProductSpace.norm_sq_eq_re_inner TrivialStar.star_trivial Pi.instTrivialStarForall instTrivialStarReal cross_dot_cross dotProduct_comm sq Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq Real.sin_sq_add_cos_sq cos_angle_mul_norm_mul_norm Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
norm_toLp_symm_crossProduct 📖	mathematical	—	Norm.norm WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.instNorm Real Fin.fintype Real.norm WithLp.toLp DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id crossProduct Real.instMul Real.sin angle PiLp.normedAddCommGroup fact_one_le_two_ennreal Real.normedAddCommGroup PiLp.innerProductSpace Real.instRCLike RCLike.toInnerProductSpaceReal	—	Nat.instAtLeastTwoHAddOfNat Function.smulCommClass Algebra.to_smulCommClass fact_one_le_two_ennreal norm_ofLp_crossProduct

---

← Back to Index