TwoDim

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

Statistics

Metric	Count
Definitions areaForm, areaForm', basisRightAngleRotation, kahler, rightAngleRotation, rightAngleRotationAux₁, rightAngleRotationAux₂	7
Theorems areaForm, kahler, rightAngleRotation, abs_areaForm_le, abs_areaForm_of_orthogonal, areaForm'_apply, areaForm_apply_self, areaForm_comp_linearIsometryEquiv, areaForm_comp_rightAngleRotation, areaForm_def, areaForm_le, areaForm_map, areaForm_map_complex, areaForm_neg_orientation, areaForm_rightAngleRotation_left, areaForm_rightAngleRotation_right, areaForm_swap, areaForm_to_volumeForm, coe_basisRightAngleRotation, eq_zero_or_eq_zero_of_kahler_eq_zero, inner_comp_rightAngleRotation, inner_mul_areaForm_sub, inner_mul_areaForm_sub', inner_mul_inner_add_areaForm_mul_areaForm, inner_mul_inner_add_areaForm_mul_areaForm', inner_rightAngleRotationAux₁_left, inner_rightAngleRotationAux₁_right, inner_rightAngleRotation_left, inner_rightAngleRotation_right, inner_rightAngleRotation_self, inner_rightAngleRotation_swap, inner_rightAngleRotation_swap', inner_sq_add_areaForm_sq, kahler_apply_apply, kahler_apply_self, kahler_comp_linearIsometryEquiv, kahler_comp_rightAngleRotation, kahler_comp_rightAngleRotation', kahler_eq_zero_iff, kahler_map, kahler_map_complex, kahler_mul, kahler_ne_zero, kahler_ne_zero_iff, kahler_neg_orientation, kahler_rightAngleRotation_left, kahler_rightAngleRotation_right, kahler_swap, linearIsometryEquiv_comp_rightAngleRotation, linearIsometryEquiv_comp_rightAngleRotation', nonneg_inner_and_areaForm_eq_zero_iff_sameRay, normSq_kahler, norm_kahler, rightAngleRotationAux₁_def, rightAngleRotationAux₁_rightAngleRotationAux₁, rightAngleRotation_def, rightAngleRotation_map, rightAngleRotation_map', rightAngleRotation_map_complex, rightAngleRotation_neg_orientation, rightAngleRotation_rightAngleRotation, rightAngleRotation_symm, rightAngleRotation_trans_neg_orientation, rightAngleRotation_trans_rightAngleRotation	64
Total	71

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
areaForm 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id Orientation.areaForm finrank_real_complex_fact orientation im instMul RingHom instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass finrank_real_complex_fact Orientation.areaForm_to_volumeForm Orientation.volumeForm_robust toBasis_orthonormalBasisOneI Matrix.det_fin_two Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.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_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one
kahler 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing Orientation.kahler finrank_real_complex_fact orientation instMul RingHom CommSemiring.toSemiring instCommSemiring RingHom.instFunLike starRingEnd instStarRing	—	smulCommClass_self finrank_real_complex_fact Algebra.to_smulCommClass Orientation.kahler_apply_apply ext mul_comm mul_neg sub_neg_eq_add ofReal_add ofReal_mul areaForm ofReal_neg MulZeroClass.mul_zero sub_zero add_zero neg_zero mul_one sub_self zero_add
rightAngleRotation 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Orientation.rightAngleRotation finrank_real_complex_fact orientation instMul I	—	ext_inner_right RingHomInvPair.ids finrank_real_complex_fact Algebra.to_smulCommClass Orientation.inner_rightAngleRotation_left areaForm map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass conj_I Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.neg_congr 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.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt

Orientation

Definitions

Name	Category	Theorems
areaForm 📖	CompOp	27 math math: Complex.areaForm, inner_mul_inner_add_areaForm_mul_areaForm, areaForm_le, areaForm_to_volumeForm, areaForm_neg_orientation, areaForm_swap, areaForm_def, areaForm'_apply, areaForm_comp_linearIsometryEquiv, nonneg_inner_and_areaForm_eq_zero_iff_sameRay, areaForm_comp_rightAngleRotation, inner_rightAngleRotation_left, inner_mul_areaForm_sub', abs_areaForm_le, abs_areaForm_of_orthogonal, inner_sq_add_areaForm_sq, areaForm_map, inner_rightAngleRotationAux₁_right, areaForm_map_complex, inner_rightAngleRotation_right, kahler_apply_apply, inner_rightAngleRotationAux₁_left, areaForm_apply_self, areaForm_rightAngleRotation_right, areaForm_rightAngleRotation_left, inner_mul_inner_add_areaForm_mul_areaForm', inner_mul_areaForm_sub
areaForm' 📖	CompOp	1 math math: areaForm'_apply
basisRightAngleRotation 📖	CompOp	2 math math: rotation_eq_matrix_toLin, coe_basisRightAngleRotation
kahler 📖	CompOp	19 math math: kahler_map_complex, Complex.kahler, kahler_comp_rightAngleRotation', kahler_eq_zero_iff, kahler_swap, kahler_comp_rightAngleRotation, kahler_neg_orientation, kahler_apply_self, kahler_rotation_left', normSq_kahler, kahler_rightAngleRotation_left, kahler_comp_linearIsometryEquiv, kahler_rotation_left, kahler_mul, kahler_map, kahler_apply_apply, kahler_rotation_right, kahler_rightAngleRotation_right, norm_kahler
rightAngleRotation 📖	CompOp	29 math math: inner_rightAngleRotation_swap', rightAngleRotation_def, rightAngleRotation_trans_rightAngleRotation, kahler_comp_rightAngleRotation, rightAngleRotation_symm, rightAngleRotation_map', inner_comp_rightAngleRotation, rightAngleRotation_rightAngleRotation, areaForm_comp_rightAngleRotation, inner_rightAngleRotation_left, linearIsometryEquiv_comp_rightAngleRotation, inner_rightAngleRotation_swap, kahler_rightAngleRotation_left, rightAngleRotation_trans_neg_orientation, coe_basisRightAngleRotation, inner_rightAngleRotation_right, rotation_apply, rightAngleRotation_map, rotation_pi_div_two, areaForm_rightAngleRotation_right, Complex.rightAngleRotation, kahler_rightAngleRotation_right, inner_rightAngleRotation_self, rotation_symm_apply, linearIsometryEquiv_comp_rightAngleRotation', rightAngleRotation_neg_orientation, rotationAux_apply, rightAngleRotation_map_complex, areaForm_rightAngleRotation_left
rightAngleRotationAux₁ 📖	CompOp	5 math math: rightAngleRotationAux₁_rightAngleRotationAux₁, rightAngleRotation_def, rightAngleRotationAux₁_def, inner_rightAngleRotationAux₁_right, inner_rightAngleRotationAux₁_left
rightAngleRotationAux₂ 📖	CompOp	1 math math: rightAngleRotation_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_areaForm_le 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass areaForm_to_volumeForm Fin.prod_univ_succ Finset.prod_congr Finset.univ_unique Matrix.cons_val_succ Matrix.cons_val_fin_one Finset.prod_const Finset.card_singleton pow_one abs_volumeForm_apply_le
abs_areaForm_of_orthogonal 📖	mathematical	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero	abs Real.lattice Real.instAddGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass areaForm_to_volumeForm abs_volumeForm_apply_of_pairwise_orthogonal Fintype.complete Matrix.cons_val_fin_one real_inner_comm Fin.prod_univ_succ Finset.prod_congr Finset.univ_unique Matrix.cons_val_succ Finset.prod_const Finset.card_singleton pow_one
areaForm'_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.funLike areaForm' LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing IsModuleTopology.toContinuousSMul Real.instAdd SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid IsTopologicalSemiring.toIsModuleTopology EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toContinuousLinearMap SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace FiniteDimensional.of_fact_finrank_eq_two Real.instDivisionRing LinearMap.instFunLike areaForm	—	Real.instIsStrictOrderedRing instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul
areaForm_apply_self 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Real.instZero	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass areaForm_to_volumeForm AlternatingMap.map_eq_zero_of_eq Matrix.cons_val_fin_one Fin.instNeZeroHAddNatOfNat_mathlib_1
areaForm_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	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 LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring Algebra.id areaForm LinearIsometryEquiv EquivLike.toFunLike LinearIsometryEquiv.instEquivLike	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Algebra.to_smulCommClass map_eq_iff_det_pos FiniteDimensional.of_fact_finrank_eq_two Fact.out Fintype.card_fin LinearIsometryEquiv.symm_apply_apply areaForm_map
areaForm_comp_rightAngleRotation 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass RingHomInvPair.ids areaForm_rightAngleRotation_right inner_rightAngleRotation_left
areaForm_def 📖	mathematical	—	areaForm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass RingHomInvPair.ids Fin.isEmpty'
areaForm_le 📖	mathematical	—	Real Real.instLE DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass areaForm_to_volumeForm Fin.prod_univ_succ Finset.prod_congr Finset.univ_unique Matrix.cons_val_succ Matrix.cons_val_fin_one Finset.prod_const Finset.card_singleton pow_one volumeForm_apply_le
areaForm_map 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Equiv Orientation Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv RingHomInvPair.ids LinearIsometryEquiv LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Fintype.complete Algebra.to_smulCommClass areaForm_to_volumeForm volumeForm_map
areaForm_map_complex 📖	mathematical	DFunLike.coe Equiv Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instInnerProductSpaceRealComplex EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex.orientation	LinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id areaForm Complex.im Complex.instMul RingHom Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing LinearIsometryEquiv LinearIsometryEquiv.instEquivLike	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Algebra.to_smulCommClass Complex.finrank_real_complex_fact Complex.areaForm areaForm_map LinearIsometryEquiv.symm_apply_apply
areaForm_neg_orientation 📖	mathematical	—	areaForm 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 LinearMap Real.semiring RingHom.id Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instNeg LinearMap.addCommGroup SeminormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing LinearMap.ext Algebra.to_smulCommClass areaForm_to_volumeForm volumeForm_neg_orientation
areaForm_rightAngleRotation_left 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Real.instNeg Inner.inner InnerProductSpace.toInner	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass RingHomInvPair.ids inner_comp_rightAngleRotation inner_rightAngleRotation_right neg_neg
areaForm_rightAngleRotation_right 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Inner.inner InnerProductSpace.toInner	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass RingHomInvPair.ids inner_rightAngleRotation_left inner_comp_rightAngleRotation
areaForm_swap 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Real.instNeg	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass areaForm_to_volumeForm Fintype.complete AlternatingMap.map_swap Fin.instNeZeroHAddNatOfNat_mathlib_1
areaForm_to_volumeForm 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm AlternatingMap AlternatingMap.instFunLike volumeForm Matrix.vecCons Matrix.vecEmpty	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass RingHomInvPair.ids Fin.isEmpty' areaForm_def Matrix.zero_empty
coe_basisRightAngleRotation 📖	mathematical	—	DFunLike.coe Module.Basis 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.instFunLike basisRightAngleRotation Matrix.vecCons LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Matrix.vecEmpty	—	Real.instIsStrictOrderedRing coe_basisOfLinearIndependentOfCardEqFinrank RingHomInvPair.ids
eq_zero_or_eq_zero_of_kahler_eq_zero 📖	mathematical	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Complex.instZero	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing smulCommClass_self NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass norm_zero norm_kahler NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
inner_comp_rightAngleRotation 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.inner_map_map
inner_mul_areaForm_sub 📖	mathematical	—	Real Real.instSub Real.instMul Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass inner_mul_areaForm_sub'
inner_mul_areaForm_sub' 📖	mathematical	—	LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedSpace LinearMap.instSub LinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id Inner.inner InnerProductSpace.toInner DFunLike.coe LinearMap.addCommMonoid LinearMap.module LinearMap.instFunLike areaForm Semifield.toCommSemiring starRingEnd RCLike.toStarRing innerₛₗ Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass inner_zero_left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass smul_zero sub_self norm_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat zero_smul Module.Basis.ext Fintype.complete areaForm_swap neg_smul sub_neg_eq_add RingHomInvPair.ids coe_basisRightAngleRotation areaForm_apply_self MulZeroClass.mul_zero inner_self_eq_norm_sq_to_K mul_comm zero_add Matrix.cons_val_fin_one areaForm_rightAngleRotation_right inner_rightAngleRotation_right neg_zero MulZeroClass.zero_mul sub_zero real_inner_comm
inner_mul_inner_add_areaForm_mul_areaForm 📖	mathematical	—	Real Real.instAdd Real.instMul Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass inner_mul_inner_add_areaForm_mul_areaForm'
inner_mul_inner_add_areaForm_mul_areaForm' 📖	mathematical	—	LinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule InnerProductSpace.toNormedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace Real.semiring SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommMonoid Real.normedField Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instAdd LinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id Inner.inner InnerProductSpace.toInner DFunLike.coe Semifield.toCommSemiring starRingEnd RCLike.toStarRing LinearMap.addCommMonoid LinearMap.module LinearMap.instFunLike innerₛₗ areaForm Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass inner_zero_left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass smul_zero add_zero norm_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat zero_smul Module.Basis.ext Fintype.complete RingHomInvPair.ids coe_basisRightAngleRotation inner_self_eq_norm_sq_to_K areaForm_apply_self mul_comm MulZeroClass.zero_mul real_inner_comm areaForm_swap neg_smul Matrix.cons_val_fin_one inner_rightAngleRotation_right neg_zero MulZeroClass.mul_zero areaForm_rightAngleRotation_right zero_add mul_neg
inner_rightAngleRotationAux₁_left 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace LinearMap.instFunLike rightAngleRotationAux₁ Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass RingHomInvPair.ids RingHomIsometric.ids instIsTopologicalAddGroupReal Real.instCompleteSpace rightAngleRotationAux₁_def RingHomInvPair.instStarRingEnd UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup InnerProductSpace.toDual_symm_apply
inner_rightAngleRotationAux₁_right 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace LinearMap.instFunLike rightAngleRotationAux₁ Real.instNeg Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass real_inner_comm inner_rightAngleRotationAux₁_left areaForm_swap
inner_rightAngleRotation_left 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation LinearMap 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 LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Algebra.to_smulCommClass rightAngleRotation_def inner_rightAngleRotationAux₁_left
inner_rightAngleRotation_right 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Real.instNeg LinearMap 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 LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Algebra.to_smulCommClass rightAngleRotation_def inner_rightAngleRotationAux₁_right
inner_rightAngleRotation_self 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Real.instZero	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Algebra.to_smulCommClass inner_rightAngleRotation_left areaForm_apply_self
inner_rightAngleRotation_swap 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Real.instNeg	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Algebra.to_smulCommClass inner_rightAngleRotation_right inner_rightAngleRotation_left
inner_rightAngleRotation_swap' 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearIsometryEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Real.instNeg	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Algebra.to_smulCommClass inner_rightAngleRotation_left inner_rightAngleRotation_swap neg_neg
inner_sq_add_areaForm_sq 📖	mathematical	—	Real Real.instAdd Monoid.toNatPow Real.instMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Real.instMul Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass sq inner_self_eq_norm_sq_to_K inner_mul_inner_add_areaForm_mul_areaForm
kahler_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Complex.instAdd Complex.ofReal Inner.inner InnerProductSpace.toInner Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike Real.instAddCommMonoid Real.normedCommRing RCLike.toInnerProductSpaceReal Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm Complex.I	—	Real.instIsStrictOrderedRing smulCommClass_self
kahler_apply_self 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing smulCommClass_self Algebra.to_smulCommClass inner_self_eq_norm_sq_to_K Complex.ofReal_pow areaForm_apply_self zero_smul add_zero
kahler_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	Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing kahler LinearIsometryEquiv EquivLike.toFunLike LinearIsometryEquiv.instEquivLike	—	Real.instIsStrictOrderedRing RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass LinearIsometryEquiv.inner_map_map areaForm_comp_linearIsometryEquiv
kahler_comp_rightAngleRotation 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation	—	Real.instIsStrictOrderedRing smulCommClass_self RingHomInvPair.ids kahler_rightAngleRotation_right kahler_rightAngleRotation_left Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Complex.I_sq 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.atom_pf Mathlib.Tactic.Ring.neg_congr 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
kahler_comp_rightAngleRotation' 📖	mathematical	—	Complex Complex.instNeg Complex.instMul Complex.I DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler	—	Real.instIsStrictOrderedRing Mathlib.Tactic.LinearCombination.eq_of_eq smulCommClass_self AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Complex.I_sq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.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.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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
kahler_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing smulCommClass_self eq_zero_or_eq_zero_of_kahler_eq_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
kahler_map 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Equiv Orientation Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv RingHomInvPair.ids LinearIsometryEquiv LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass areaForm_map LinearIsometryEquiv.inner_map_map
kahler_map_complex 📖	mathematical	DFunLike.coe Equiv Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instInnerProductSpaceRealComplex EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex.orientation	LinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Complex.instNormedAddCommGroup LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Complex.instMul LinearIsometryEquiv LinearIsometryEquiv.instEquivLike RingHom CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	Real.instIsStrictOrderedRing RingHomInvPair.ids smulCommClass_self Complex.finrank_real_complex_fact Complex.kahler kahler_map LinearIsometryEquiv.symm_apply_apply
kahler_mul 📖	mathematical	—	Complex Complex.instMul DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing smulCommClass_self Complex.ext Algebra.to_smulCommClass real_inner_comm areaForm_swap Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd inner_mul_inner_add_areaForm_mul_areaForm 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.atom_pf Mathlib.Tactic.Ring.neg_congr 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.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero 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_add inner_mul_areaForm_sub
kahler_ne_zero 📖	—	—	—	—	Real.instIsStrictOrderedRing smulCommClass_self eq_zero_or_eq_zero_of_kahler_eq_zero
kahler_ne_zero_iff 📖	—	—	—	—	Real.instIsStrictOrderedRing smulCommClass_self Mathlib.Tactic.Contrapose.contrapose₂ Algebra.to_smulCommClass inner_zero_left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass MulZeroClass.zero_mul add_zero inner_zero_right kahler_ne_zero
kahler_neg_orientation 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Orientation Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing instNegRay AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Real.instAddCommGroup AlternatingMap.instModule RingHom Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	Real.instIsStrictOrderedRing smulCommClass_self Algebra.to_smulCommClass areaForm_neg_orientation neg_smul map_add SemilinearMapClass.toAddHomClass Complex.instCharZero RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass Complex.conj_ofReal map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Complex.conj_I mul_neg
kahler_rightAngleRotation_left 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Complex.instMul Complex.instNeg Complex.I	—	Real.instIsStrictOrderedRing smulCommClass_self RingHomInvPair.ids Algebra.to_smulCommClass inner_rightAngleRotation_left areaForm_rightAngleRotation_left Complex.ofReal_neg Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Complex.I_sq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.one_mul 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.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
kahler_rightAngleRotation_right 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler LinearIsometryEquiv RingHomInvPair.ids EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Complex.instMul Complex.I	—	Real.instIsStrictOrderedRing smulCommClass_self RingHomInvPair.ids Algebra.to_smulCommClass inner_rightAngleRotation_right Complex.ofReal_neg areaForm_rightAngleRotation_right Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Complex.I_sq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
kahler_swap 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler RingHom CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	Real.instIsStrictOrderedRing smulCommClass_self Algebra.to_smulCommClass real_inner_comm areaForm_swap neg_smul map_add SemilinearMapClass.toAddHomClass Complex.instCharZero RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass Complex.conj_ofReal map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Complex.conj_I mul_neg
linearIsometryEquiv_comp_rightAngleRotation 📖	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	LinearIsometryEquiv EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation	—	Real.instIsStrictOrderedRing RingHomInvPair.ids LinearIsometryEquiv.symm_apply_apply map_eq_iff_det_pos FiniteDimensional.of_fact_finrank_eq_two Fact.out Fintype.card_fin rightAngleRotation_map
linearIsometryEquiv_comp_rightAngleRotation' 📖	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	LinearIsometryEquiv.trans RingHomCompTriple.ids rightAngleRotation	—	Real.instIsStrictOrderedRing RingHomInvPair.ids LinearIsometryEquiv.ext RingHomCompTriple.ids linearIsometryEquiv_comp_rightAngleRotation
nonneg_inner_and_areaForm_eq_zero_iff_sameRay 📖	mathematical	—	Real Real.instLE Real.instZero Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id areaForm SameRay Real.partialOrder Real.instIsStrictOrderedRing	—	Real.instIsStrictOrderedRing Algebra.to_smulCommClass inner_zero_left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass SameRay.congr_simp RingHomInvPair.ids nonneg_of_mul_nonneg_left IsStrictOrderedRing.toMulPosStrictMono pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass norm_pos_iff eq_zero_of_ne_zero_of_mul_right_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass pow_ne_zero isReduced_of_noZeroDivisors LT.lt.ne' SameRay.add_right SameRay.sameRay_nonneg_smul_right PosSMulMono.toSMulPosMono Real.instIsOrderedRing Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule IsScalarTower.left zero_smul Module.Basis.sum_repr Finset.sum_congr coe_basisRightAngleRotation Fin.sum_univ_succ Fin.succ_zero_eq_one' Finset.univ_eq_empty Fin.isEmpty' add_zero inner_add_right real_inner_smul_right real_inner_self_eq_norm_sq inner_rightAngleRotation_right areaForm_apply_self neg_zero MulZeroClass.mul_zero map_add SemilinearMapClass.toAddHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass areaForm_rightAngleRotation_right zero_add SameRay.exists_nonneg_left inner_smul_right MulActionSemiHomClass.map_smulₛₗ mul_nonneg IsOrderedRing.toPosMulMono le_of_lt
normSq_kahler 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Complex Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq LinearMap RingHom.id ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing smulCommClass_self Algebra.to_smulCommClass MulZeroClass.mul_zero mul_one sub_self add_zero zero_add sq inner_sq_add_areaForm_sq
norm_kahler 📖	mathematical	—	Norm.norm Complex Complex.instNorm DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing instInnerProductSpaceRealComplex LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing kahler Real.instMul NormedAddCommGroup.toNorm	—	Real.instIsStrictOrderedRing smulCommClass_self sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg mul_nonneg IsOrderedRing.toPosMulMono Complex.sq_norm Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd normSq_kahler Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
rightAngleRotationAux₁_def 📖	mathematical	—	rightAngleRotationAux₁	—	Real.instIsStrictOrderedRing RingHomInvPair.ids instIsTopologicalAddGroupReal Real.instCompleteSpace
rightAngleRotationAux₁_rightAngleRotationAux₁ 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike LinearMap.instFunLike rightAngleRotationAux₁ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing ext_inner_left LinearIsometry.inner_map_map Algebra.to_smulCommClass inner_rightAngleRotationAux₁_right inner_rightAngleRotationAux₁_left inner_neg_right
rightAngleRotation_def 📖	mathematical	—	rightAngleRotation LinearIsometryEquiv.ofLinearIsometry Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike rightAngleRotationAux₂ LinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instNeg SeminormedAddCommGroup.toAddCommGroup rightAngleRotationAux₁	—	Real.instIsStrictOrderedRing RingHomInvPair.ids
rightAngleRotation_map 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Equiv Orientation Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv LinearIsometryEquiv.symm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids ext_inner_right Algebra.to_smulCommClass inner_rightAngleRotation_left areaForm_map LinearIsometryEquiv.inner_map_map LinearIsometryEquiv.apply_symm_apply
rightAngleRotation_map' 📖	mathematical	—	rightAngleRotation DFunLike.coe Equiv Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearIsometryEquiv.trans RingHomCompTriple.ids LinearIsometryEquiv.symm	—	Real.instIsStrictOrderedRing RingHomInvPair.ids LinearIsometryEquiv.ext RingHomCompTriple.ids rightAngleRotation_map
rightAngleRotation_map_complex 📖	mathematical	DFunLike.coe Equiv Orientation Real Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instInnerProductSpaceRealComplex EquivLike.toFunLike Equiv.instEquivLike map LinearIsometryEquiv.toLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex.orientation	LinearIsometryEquiv LinearIsometryEquiv.instEquivLike rightAngleRotation Complex.instMul Complex.I	—	Real.instIsStrictOrderedRing RingHomInvPair.ids Complex.finrank_real_complex_fact Complex.rightAngleRotation rightAngleRotation_map LinearIsometryEquiv.symm_apply_apply
rightAngleRotation_neg_orientation 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation Orientation Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNegRay Real.commRing AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule AlternatingMap.instAddCommGroup Real.instAddCommGroup AlternatingMap.instModule NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing ext_inner_right RingHomInvPair.ids Algebra.to_smulCommClass inner_rightAngleRotation_left areaForm_neg_orientation inner_neg_left
rightAngleRotation_rightAngleRotation 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike rightAngleRotation NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Real.instIsStrictOrderedRing RingHomInvPair.ids rightAngleRotation_def rightAngleRotationAux₁_rightAngleRotationAux₁
rightAngleRotation_symm 📖	mathematical	—	LinearIsometryEquiv.symm Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike rightAngleRotation LinearIsometryEquiv.trans RingHomCompTriple.ids LinearIsometryEquiv.neg	—	Real.instIsStrictOrderedRing RingHomInvPair.ids RingHomCompTriple.ids rightAngleRotation_def LinearIsometryEquiv.toLinearIsometry_injective
rightAngleRotation_trans_neg_orientation 📖	mathematical	—	rightAngleRotation 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 LinearIsometryEquiv.trans Real.semiring RingHom.id RingHomInvPair.ids RingHomCompTriple.ids LinearIsometryEquiv.neg	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids rightAngleRotation_neg_orientation
rightAngleRotation_trans_rightAngleRotation 📖	mathematical	—	LinearIsometryEquiv.trans Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike rightAngleRotation LinearIsometryEquiv.neg	—	Real.instIsStrictOrderedRing LinearIsometryEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids rightAngleRotation_rightAngleRotation

---

← Back to Index