Basic

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

Statistics

Metric	Count
Definitions angle	1
Theorems angle_add_angle_eq_pi_of_angle_eq_pi, angle_comm, angle_eq_pi_iff, angle_eq_zero_iff, angle_le_pi, angle_neg_left, angle_neg_neg, angle_neg_right, angle_neg_self_of_nonzero, angle_nonneg, angle_normalize_left, angle_normalize_right, angle_self, angle_self_neg_of_nonzero, angle_smul_left_of_neg, angle_smul_left_of_pos, angle_smul_right_of_neg, angle_smul_right_of_pos, angle_smul_smul, angle_zero_left, angle_zero_right, continuousAt_angle, cos_angle, cos_angle_mul_norm_mul_norm, cos_eq_neg_one_iff_angle_eq_pi, cos_eq_one_iff_angle_eq_zero, cos_eq_zero_iff_angle_eq_pi_div_two, eq_of_angle_eq_zero_of_norm_eq, inner_eq_cos_angle_of_norm_eq_one, inner_eq_mul_norm_iff_angle_eq_zero, inner_eq_mul_norm_of_angle_eq_zero, inner_eq_neg_mul_norm_iff_angle_eq_pi, inner_eq_neg_mul_norm_of_angle_eq_pi, inner_eq_zero_iff_angle_eq_pi_div_two, norm_add_eq_add_norm_iff_angle_eq_zero, norm_add_eq_add_norm_of_angle_eq_zero, norm_add_eq_norm_sub_iff_angle_eq_pi_div_two, norm_sub_eq_abs_sub_norm_iff_angle_eq_zero, norm_sub_eq_abs_sub_norm_of_angle_eq_zero, norm_sub_eq_add_norm_iff_angle_eq_pi, norm_sub_eq_add_norm_of_angle_eq_pi, sin_angle, sin_angle_add, sin_angle_mul_norm_mul_norm, sin_angle_nonneg, sin_eq_one_iff_angle_eq_pi_div_two, sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, angle_map, angle_coe	49
Total	50

InnerProductGeometry

Definitions

Name	Category	Theorems
angle 📖	CompOp	111 math math: cos_angle_add_of_inner_eq_zero, angle_add_angle_sub_add_angle_sub_eq_pi, angle_neg_self_of_nonzero, Complex.norm_sub_mem_Icc_angle, angle_normalize_left, angle_sub_eq_arccos_of_inner_eq_zero, sin_angle, Complex.angle_exp_one, Complex.angle_div_right_eq_angle_mul_left, angle_smul_right_of_pos, norm_div_cos_angle_sub_of_inner_eq_zero, angle_smul_left_of_neg, angle_normalize_right, Complex.angle_mul_left, tan_angle_sub_mul_norm_of_inner_eq_zero, Complex.mul_angle_le_norm_sub, sin_angle_div_norm_eq_sin_angle_div_norm, norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, Orientation.oangle_eq_pi_iff_angle_eq_pi, angle_le_pi, norm_add_eq_norm_sub_iff_angle_eq_pi_div_two, tan_angle_add_mul_norm_of_inner_eq_zero, sin_angle_mul_norm_eq_sin_angle_mul_norm, norm_add_eq_add_norm_iff_angle_eq_zero, Orientation.oangle_eq_angle_or_eq_neg_angle, angle_neg_right, sin_angle_nonneg, angle_zero_right, sin_eq_one_iff_angle_eq_pi_div_two, norm_toLp_symm_crossProduct, angle_add_le_pi_div_two_of_inner_eq_zero, Orientation.angle_eq_iff_oangle_eq_or_sameRay, angle_eq_zero_iff, cos_angle, angle_add_eq_arctan_of_inner_eq_zero, cos_angle_mul_norm_mul_norm, Complex.angle_mul_right, sin_angle_sub_of_inner_eq_zero, Orientation.oangle_eq_zero_iff_angle_eq_zero, angle_self, sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, norm_div_tan_angle_sub_of_inner_eq_zero, Complex.angle_eq_abs_arg, inner_eq_neg_mul_norm_iff_angle_eq_pi, cos_eq_zero_iff_angle_eq_pi_div_two, angle_sub_le_pi_div_two_of_inner_eq_zero, angle_zero_left, cos_eq_neg_one_iff_angle_eq_pi, norm_ofLp_crossProduct, norm_div_sin_angle_add_of_inner_eq_zero, cos_angle_sub_of_inner_eq_zero, norm_div_tan_angle_add_of_inner_eq_zero, angle_le_angle_add_angle, tan_angle_sub_of_inner_eq_zero, angle_smul_right_of_neg, sin_angle_sub_mul_norm_of_inner_eq_zero, angle_add_lt_pi_div_two_of_inner_eq_zero, norm_sub_eq_add_norm_iff_angle_eq_pi, angle_add_pos_of_inner_eq_zero, tan_angle_add_of_inner_eq_zero, Complex.norm_sub_le_angle, Orientation.oangle_eq_angle_of_sign_eq_one, Complex.angle_div_left_eq_angle_mul_right, angle_eq_angle_add_angle_iff, angle_nonneg, Orientation.cos_oangle_eq_cos_angle, angle_self_neg_of_nonzero, norm_div_sin_angle_sub_of_inner_eq_zero, Complex.angle_le_mul_norm_sub, angle_smul_smul, angle_sub_lt_pi_div_two_of_inner_eq_zero, cos_angle_add_mul_norm_of_inner_eq_zero, angle_sub_pos_of_inner_eq_zero, Orientation.angle_eq_iff_oangle_eq_of_sign_eq, angle_comm, angle_add_eq_arccos_of_inner_eq_zero, norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, norm_sub_eq_abs_sub_norm_iff_angle_eq_zero, Orientation.angle_eq_abs_oangle_toReal, sin_angle_add_of_inner_eq_zero, angle_sub_eq_arcsin_of_inner_eq_zero, Complex.angle_one_left, Complex.angle_one_right, cos_eq_one_iff_angle_eq_zero, Submodule.angle_coe, Orientation.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg, angle_sub_eq_arctan_of_inner_eq_zero, norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle, cos_angle_sub_mul_norm_of_inner_eq_zero, angle_sub_eq_angle_sub_rev_of_norm_eq, angle_eq_pi_iff, angle_neg_neg, inner_eq_cos_angle_of_norm_eq_one, continuousAt_angle, sin_angle_add, angle_add_eq_arcsin_of_inner_eq_zero, sin_angle_add_mul_norm_of_inner_eq_zero, inner_eq_zero_iff_angle_eq_pi_div_two, IsConformalMap.preserves_angle, angle_eq_angle_add_add_angle_add_of_mem_span, Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero, sin_angle_mul_norm_mul_norm, Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one, LinearIsometry.angle_map, inner_eq_mul_norm_iff_angle_eq_zero, ConformalAt.preserves_angle, angle_smul_left_of_pos, angle_neg_left, angle_eq_angle_add_add_angle_add, Complex.angle_exp_exp, norm_div_cos_angle_add_of_inner_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_add_angle_eq_pi_of_angle_eq_pi 📖	mathematical	angle Real.pi	Real Real.instAdd	—	angle_eq_pi_iff angle_smul_left_of_neg angle_neg_left add_sub_cancel
angle_comm 📖	mathematical	—	angle	—	real_inner_comm mul_comm
angle_eq_pi_iff 📖	mathematical	—	angle Real.pi Real Real.instLT Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	angle.eq_1 real_inner_div_norm_mul_norm_eq_neg_one_iff Real.arccos_eq_pi LE.le.ge_iff_eq' abs_le Real.instIsOrderedAddMonoid abs_real_inner_div_norm_mul_norm_le_one
angle_eq_zero_iff 📖	mathematical	—	angle Real Real.instZero Real.instLT SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	angle.eq_1 real_inner_div_norm_mul_norm_eq_one_iff Real.arccos_eq_zero LE.le.ge_iff_eq' abs_le Real.instIsOrderedAddMonoid abs_real_inner_div_norm_mul_norm_le_one
angle_le_pi 📖	mathematical	—	Real Real.instLE angle Real.pi	—	Real.arccos_le_pi
angle_neg_left 📖	mathematical	—	angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instSub Real.pi	—	angle_neg_neg neg_neg angle_neg_right
angle_neg_neg 📖	mathematical	—	angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	inner_neg_neg norm_neg
angle_neg_right 📖	mathematical	—	angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instSub Real.pi	—	Real.arccos_neg norm_neg inner_neg_right neg_div
angle_neg_self_of_nonzero 📖	mathematical	—	angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.pi	—	angle_comm angle_self_neg_of_nonzero
angle_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero angle	—	Real.arccos_nonneg
angle_normalize_left 📖	mathematical	—	angle NormedSpace.normalize InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat NormedSpace.normalize_zero_eq_zero angle_zero_left NormedSpace.normalize.eq_1 angle_smul_left_of_pos inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff
angle_normalize_right 📖	mathematical	—	angle NormedSpace.normalize InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	angle_comm angle_normalize_left
angle_self 📖	mathematical	—	angle Real Real.instZero	—	real_inner_self_eq_norm_mul_norm div_self inner_self_ne_zero Real.arccos_one
angle_self_neg_of_nonzero 📖	mathematical	—	angle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.pi	—	angle_neg_right angle_self sub_zero
angle_smul_left_of_neg 📖	mathematical	Real Real.instLT Real.instZero	angle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	angle_comm angle_smul_right_of_neg
angle_smul_left_of_pos 📖	mathematical	Real Real.instLT Real.instZero	angle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	angle_comm angle_smul_right_of_pos
angle_smul_right_of_neg 📖	mathematical	Real Real.instLT Real.instZero	angle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg_neg neg_smul angle_neg_right angle_smul_right_of_pos neg_pos_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
angle_smul_right_of_pos 📖	mathematical	Real Real.instLT Real.instZero	angle SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	inner_smul_right norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_lt mul_assoc mul_comm mul_div_mul_left ne_of_gt
angle_smul_smul 📖	mathematical	—	angle Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass angle.eq_1 real_inner_smul_left inner_smul_right norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs mul_mul_mul_comm abs_mul_abs_self mul_assoc mul_div_mul_left
angle_zero_left 📖	mathematical	—	angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat inner_zero_left zero_div Real.arccos_zero
angle_zero_right 📖	mathematical	—	angle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat inner_zero_right zero_div Real.arccos_zero
continuousAt_angle 📖	mathematical	—	ContinuousAt Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.pseudoMetricSpace angle	—	ContinuousAt.comp' Continuous.continuousAt Real.continuous_arccos ContinuousAt.div₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousAt.inner ContinuousAt.fst continuousAt_id' ContinuousAt.snd ContinuousAt.fun_mul ContinuousAt.norm NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
cos_angle 📖	mathematical	—	Real.cos angle Real DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	Real.cos_arccos abs_le Real.instIsOrderedAddMonoid abs_real_inner_div_norm_mul_norm_le_one
cos_angle_mul_norm_mul_norm 📖	mathematical	—	Real Real.instMul Real.cos angle Norm.norm NormedAddCommGroup.toNorm Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	cos_angle div_mul_cancel_of_imp NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass inner_zero_left inner_zero_right
cos_eq_neg_one_iff_angle_eq_pi 📖	mathematical	—	Real.cos angle Real Real.instNeg Real.instOne Real.pi	—	Real.cos_pi Set.InjOn.eq_iff Real.injOn_cos angle_nonneg angle_le_pi Set.right_mem_Icc LT.lt.le Real.pi_pos
cos_eq_one_iff_angle_eq_zero 📖	mathematical	—	Real.cos angle Real Real.instOne Real.instZero	—	Real.cos_zero Set.InjOn.eq_iff Real.injOn_cos angle_nonneg angle_le_pi Set.left_mem_Icc LT.lt.le Real.pi_pos
cos_eq_zero_iff_angle_eq_pi_div_two 📖	mathematical	—	Real.cos angle Real Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Real.cos_pi_div_two Set.InjOn.eq_iff Real.injOn_cos angle_nonneg angle_le_pi le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero 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.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Real.pi_pos Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq
eq_of_angle_eq_zero_of_norm_eq 📖	—	angle Real Real.instZero Norm.norm NormedAddCommGroup.toNorm	—	—	—
inner_eq_cos_angle_of_norm_eq_one 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.cos angle	—	cos_angle mul_one div_one
inner_eq_mul_norm_iff_angle_eq_zero 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm angle Real.instZero	—	LT.lt.ne' mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff angle.eq_1 div_self Real.arccos_one inner_eq_mul_norm_of_angle_eq_zero
inner_eq_mul_norm_of_angle_eq_zero 📖	mathematical	angle Real Real.instZero	Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	Real.cos_zero one_mul
inner_eq_neg_mul_norm_iff_angle_eq_pi 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instNeg Real.instMul Norm.norm NormedAddCommGroup.toNorm angle Real.pi	—	LT.lt.ne' mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff angle.eq_1 neg_div div_self Real.arccos_neg_one inner_eq_neg_mul_norm_of_angle_eq_pi
inner_eq_neg_mul_norm_of_angle_eq_pi 📖	mathematical	angle Real.pi	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instNeg Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	Real.cos_pi neg_mul one_mul
inner_eq_zero_iff_angle_eq_pi_div_two 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero angle DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass inner_zero_left inner_zero_right
norm_add_eq_add_norm_iff_angle_eq_zero 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real Real.instAdd angle Real.instZero	—	inner_eq_mul_norm_iff_angle_eq_zero Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_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_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf 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.Tactic.Ring.neg_zero 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 Mathlib.Tactic.Linarith.lt_of_eq_of_lt neg_eq_zero sub_eq_zero_of_eq norm_add_pow_two_real sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.pow_subst CancelDenoms.add_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz norm_add_eq_add_norm_of_angle_eq_zero
norm_add_eq_add_norm_of_angle_eq_zero 📖	mathematical	angle Real Real.instZero	Norm.norm NormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAdd	—	sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat norm_add_pow_two_real inner_eq_mul_norm_of_angle_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_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_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf
norm_add_eq_norm_sub_iff_angle_eq_pi_div_two 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup angle Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg inner_eq_zero_iff_angle_eq_pi_div_two norm_add_pow_two_real norm_sub_pow_two_real Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_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_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_eq_of_lt neg_eq_zero sub_eq_zero_of_eq Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Linarith.mul_eq
norm_sub_eq_abs_sub_norm_iff_angle_eq_zero 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup abs Real Real.lattice Real.instAddGroup Real.instSub angle Real.instZero	—	inner_eq_mul_norm_iff_angle_eq_zero sq_abs Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_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_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one 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.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_eq_of_lt sub_eq_zero_of_eq norm_sub_pow_two_real CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.pow_subst CancelDenoms.add_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Tactic.Linarith.mul_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Ring.neg_congr neg_eq_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz norm_sub_eq_abs_sub_norm_of_angle_eq_zero
norm_sub_eq_abs_sub_norm_of_angle_eq_zero 📖	mathematical	angle Real Real.instZero	Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup abs Real.lattice Real.instAddGroup Real.instSub	—	sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Nat.instAtLeastTwoHAddOfNat norm_sub_pow_two_real inner_eq_mul_norm_of_angle_eq_zero sq_abs Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_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_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one 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_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add
norm_sub_eq_add_norm_iff_angle_eq_pi 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real Real.instAdd angle Real.pi	—	inner_eq_neg_mul_norm_iff_angle_eq_pi Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_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_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one 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.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf 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 Mathlib.Tactic.Linarith.lt_of_eq_of_lt sub_eq_zero_of_eq norm_sub_pow_two_real sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.add_subst CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Ring.neg_congr neg_eq_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz norm_sub_eq_add_norm_of_angle_eq_pi
norm_sub_eq_add_norm_of_angle_eq_pi 📖	mathematical	angle Real.pi	Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real Real.instAdd	—	sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat norm_sub_pow_two_real inner_eq_neg_mul_norm_of_angle_eq_pi Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_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_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_pf_right 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.sub_pf 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.mul_one
sin_angle 📖	mathematical	—	Real.sin angle Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.sqrt Real.instSub Real.instMul Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Norm.norm NormedAddCommGroup.toNorm	—	sin_angle_mul_norm_mul_norm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul 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 Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt norm_pos_iff one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf
sin_angle_add 📖	mathematical	—	Real.sin angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.sqrt Real.instSub Real.instMul Inner.inner InnerProductSpace.toInner Real.instRCLike Norm.norm NormedAddCommGroup.toNorm	—	sin_angle Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul 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 Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt norm_pos_iff one_ne_zero NeZero.one GroupWithZero.toNontrivial inner_add_right inner_add_left real_inner_comm Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one 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.Tactic.Ring.neg_zero 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 Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.RingNF.add_neg
sin_angle_mul_norm_mul_norm 📖	mathematical	—	Real Real.instMul Real.sin angle Norm.norm NormedAddCommGroup.toNorm Real.sqrt Real.instSub Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	Real.sin_arccos Real.sqrt_sq mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg Real.sqrt_mul' Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul sq eq_or_ne inner_zero_left norm_zero MulZeroClass.zero_mul div_zero MulZeroClass.mul_zero sub_zero zero_pow Nat.instCharZero Real.sqrt_zero inner_self_eq_norm_sq_to_K sub_self inner_zero_right real_inner_self_eq_norm_mul_norm 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.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt norm_pos_iff one_mul 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'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial
sin_angle_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero Real.sin angle	—	Real.sin_nonneg_of_nonneg_of_le_pi angle_nonneg angle_le_pi
sin_eq_one_iff_angle_eq_pi_div_two 📖	mathematical	—	Real.sin angle Real Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat cos_eq_zero_iff_angle_eq_pi_div_two abs_eq_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Real.abs_cos_eq_sqrt_one_sub_sin_sq one_pow sub_self Real.sqrt_zero Real.sin_pi_div_two
sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi 📖	mathematical	—	Real.sin angle Real Real.instZero Real.pi	—	Real.sin_eq_zero_iff_cos_eq cos_eq_one_iff_angle_eq_zero cos_eq_neg_one_iff_angle_eq_pi

LinearIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_map 📖	mathematical	—	InnerProductGeometry.angle DFunLike.coe LinearIsometry Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instFunLike	—	InnerProductGeometry.angle.eq_1 inner_map_map norm_map

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_coe 📖	mathematical	—	InnerProductGeometry.angle Submodule 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 SetLike.instMembership setLike normedAddCommGroup Real.instRing innerProductSpace	—	LinearIsometry.angle_map

---

← Back to Index