Isometry

📁 Source: Mathlib/Analysis/Complex/Isometry.lean

Statistics

Metric	Count
Definitions rotation, rotationOf	2
Theorems im_apply_eq_im, im_apply_eq_im_or_neg_of_re_apply_eq_re, re_apply_eq_re, re_apply_eq_re_of_add_conj_eq, det_rotation, linearEquiv_det_rotation, linear_isometry_complex, linear_isometry_complex_aux, rotationOf_coe, rotationOf_rotation, rotation_apply, rotation_injective, rotation_ne_conjLIE, rotation_symm, rotation_trans, toMatrix_rotation	16
Total	18

LinearIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
im_apply_eq_im 📖	mathematical	DFunLike.coe LinearIsometry Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace instFunLike Complex.instOne	Complex.instAdd RingHom CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	norm_map map_sub add_comm add_sub Complex.ofReal_pow map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one sub_sub Complex.normSq_eq_norm_sq Complex.mul_conj mul_sub sub_mul one_mul map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass Complex.instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat
im_apply_eq_im_or_neg_of_re_apply_eq_re 📖	mathematical	Complex.re DFunLike.coe LinearIsometry Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace instFunLike	Complex.im Real.instNeg	—	norm_map mul_self_eq_mul_self_iff NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass add_left_cancel_iff AddLeftCancelSemigroup.toIsLeftCancelAdd Complex.normSq_apply Complex.normSq_nonneg
re_apply_eq_re 📖	mathematical	DFunLike.coe LinearIsometry Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace instFunLike Complex.instOne	Complex.re	—	re_apply_eq_re_of_add_conj_eq im_apply_eq_im
re_apply_eq_re_of_add_conj_eq 📖	mathematical	Complex Complex.instAdd DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing LinearIsometry Real Real.semiring RingHom.id NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace instFunLike	Complex.re	—	Nat.instAtLeastTwoHAddOfNat IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain RCLike.charZero_rclike add_neg_cancel

(root)

Definitions

Name	Category	Theorems
rotation 📖	CompOp	9 math math: rotation_injective, rotation_apply, toMatrix_rotation, linear_isometry_complex, rotationOf_rotation, rotation_trans, linearEquiv_det_rotation, det_rotation, rotation_symm
rotationOf 📖	CompOp	2 math math: rotationOf_rotation, rotationOf_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_rotation 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring Complex AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap Real.semiring RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv Circle LinearIsometryEquiv Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup rotation Real.instOne	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.det_toMatrix toMatrix_rotation Matrix.det_fin_two Matrix.cons_val' Matrix.cons_val_fin_one neg_mul sub_neg_eq_add Circle.normSq_coe
linearEquiv_det_rotation 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det LinearIsometryEquiv.toLinearEquiv Real.semiring Circle LinearIsometryEquiv CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup rotation Units.instOne	—	RingHomInvPair.ids LinearEquiv.coe_det det_rotation Units.val_one
linear_isometry_complex 📖	mathematical	—	DFunLike.coe MonoidHom Circle LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup MonoidHom.instFunLike rotation LinearIsometryEquiv.trans RingHomCompTriple.ids Complex.conjLIE	—	RingHomInvPair.ids sub_zero LinearIsometryEquiv.norm_map CStarRing.norm_of_mem_unitary RCLike.instCStarRing Complex.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass RingHomCompTriple.ids LinearIsometryEquiv.trans.congr_simp rotation_symm map_inv MonoidHom.instMonoidHomClass inv_mul_cancel₀ EquivLike.toEmbeddingLike AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass NeZero.charZero_one Complex.instCharZero rotation_apply LinearIsometryEquiv.mul_refl eq_mul_of_inv_mul_eq linear_isometry_complex_aux
linear_isometry_complex_aux 📖	mathematical	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Complex.instOne	LinearIsometryEquiv.refl Complex.conjLIE	—	RingHomInvPair.ids neg_zero Complex.I_re LinearIsometry.re_apply_eq_re LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re LinearIsometryEquiv.toLinearEquiv_injective Module.Basis.ext' Fintype.complete Complex.coe_basisOneI Matrix.cons_val_fin_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Complex.conj_I
rotationOf_coe 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere rotationOf DivInvMonoid.toDiv Complex.instDivInvMonoid DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id RingHomInvPair.ids NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike Complex.instOne Complex.ofReal Norm.norm Complex.instNorm	—	RingHomInvPair.ids
rotationOf_rotation 📖	mathematical	—	rotationOf DFunLike.coe MonoidHom Circle LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup MonoidHom.instFunLike rotation	—	RingHomInvPair.ids mul_one norm_eq_of_mem_sphere div_one
rotation_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike MonoidHom Circle MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup MonoidHom.instFunLike rotation Complex.instMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere	—	RingHomInvPair.ids
rotation_injective 📖	mathematical	—	Circle LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup MonoidHom.instFunLike rotation	—	RingHomInvPair.ids rotationOf_rotation
rotation_ne_conjLIE 📖	—	—	—	—	RingHomInvPair.ids LinearIsometryEquiv.congr_fun one_ne_zero NeZero.charZero_one Complex.instCharZero CharZero.eq_neg_self_iff NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass mul_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass rotation_apply mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Complex.I_ne_zero neg_one_mul Complex.conj_I
rotation_symm 📖	mathematical	—	LinearIsometryEquiv.symm Real Complex Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace DFunLike.coe MonoidHom Circle LinearIsometryEquiv MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup MonoidHom.instFunLike rotation InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	LinearIsometryEquiv.ext RingHomInvPair.ids
rotation_trans 📖	mathematical	—	LinearIsometryEquiv.trans Real Complex Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace DFunLike.coe MonoidHom Circle LinearIsometryEquiv MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup MonoidHom.instFunLike rotation MulOne.toMul	—	LinearIsometryEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
toMatrix_rotation 📖	mathematical	—	DFunLike.coe LinearEquiv Real CommSemiring.toSemiring Real.instCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Complex.commRing Algebra.toModule Complex.instSemiring Complex.instAlgebraOfReal Algebra.id Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Fin.fintype Finite.of_fintype Complex.basisOneI LinearEquiv.toLinearMap Real.semiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule Real.normedField NormedSpace.complexToReal NormedField.toNormedSpace LinearIsometryEquiv.toLinearEquiv MonoidHom Circle LinearIsometryEquiv MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup LinearIsometryEquiv.instGroup MonoidHom.instFunLike rotation Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.instField Matrix.planeConformalMatrix Complex.re Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Complex.im	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.toMatrix_apply Complex.coe_basisOneI Matrix.cons_val' Matrix.empty_val' Matrix.cons_val_fin_one Fintype.complete mul_one MulZeroClass.mul_zero sub_zero zero_add zero_sub add_zero

---

← Back to Index