ProjectiveLine

📁 Source: Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean

Statistics

Metric	Count
Definitions parabolicFixedPoint, equivProjectivization, instGLAction, instModuleMatrixFinOfNatNatProd	4
Theorems smul_ne_self, parabolicFixedPoint_pow, smul_eq_self_iff, fin_two_smul_prod, fixpointPolynomial_aeval_eq_zero_iff, fin_two_smul_prod, equivProjectivization_apply_coe, equivProjectivization_apply_infinity, equivProjectivization_symm_apply_mk, map_smul, smul_infty_def, smul_infty_eq_ite, smul_infty_eq_self_iff, smul_some_eq_ite, instSMulCommClassMatrixFinOfNatNatProd	15
Total	19

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fin_two_smul_prod 📖	mathematical	—	Matrix SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Prod.instAddZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Fin.fintype Prod.instAddMonoid Module.toDistribMulAction Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleMatrixFinOfNatNatProd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul	—	RingHomInvPair.ids LinearEquiv.left_inv LinearEquiv.right_inv mulVec_eq_sum Fin.sum_univ_two cons_val_fin_one

Matrix.GeneralLinearGroup

Definitions

Name	Category	Theorems
parabolicFixedPoint 📖	CompOp	2 math math: IsParabolic.parabolicFixedPoint_pow, IsParabolic.smul_eq_self_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fin_two_smul_prod 📖	mathematical	—	Matrix.GeneralLinearGroup Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Units.instSMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Prod.instAddZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Prod.instAddMonoid Module.toDistribMulAction Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instModuleMatrixFinOfNatNatProd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul Units.val	—	Matrix.fin_two_smul_prod
fixpointPolynomial_aeval_eq_zero_iff 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval fixpointPolynomial EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.GeneralLinearGroup Fin.fintype OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction OnePoint.instGLAction OnePoint.some	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass Polynomial.aeval_C Polynomial.aeval_X_pow Polynomial.aeval_X OnePoint.smul_some_eq_ite det_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing Matrix.det_fin_two OnePoint.infty_ne_coe OnePoint.coe_eq_coe div_eq_iff

Matrix.GeneralLinearGroup.IsElliptic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_ne_self 📖	—	Matrix.GeneralLinearGroup.IsElliptic EuclideanDomain.toCommRing Field.toEuclideanDomain PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	OnePoint.smul_infty_eq_self_iff not_le_of_gt Nat.instAtLeastTwoHAddOfNat Matrix.discr_fin_two Matrix.trace_fin_two Matrix.det_fin_two sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid sq sub_eq_add_neg map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_neg Polynomial.eval_add Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_X Polynomial.eval_neg discrim_eq_sq_of_quadratic_eq_zero

Matrix.GeneralLinearGroup.IsParabolic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
parabolicFixedPoint_pow 📖	mathematical	Matrix.GeneralLinearGroup.IsParabolic EuclideanDomain.toCommRing Field.toEuclideanDomain	Matrix.GeneralLinearGroup.parabolicFixedPoint Matrix.GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Monoid.toNatPow Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	—	smul_eq_self_iff pow CharZero.NeZero.two pow_zero one_smul pow_succ SemigroupAction.mul_smul
smul_eq_self_iff 📖	mathematical	Matrix.GeneralLinearGroup.IsParabolic EuclideanDomain.toCommRing Field.toEuclideanDomain	Matrix.GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction OnePoint.instGLAction Matrix.GeneralLinearGroup.parabolicFixedPoint	—	Nat.instAtLeastTwoHAddOfNat OnePoint.smul_infty_eq_ite Matrix.det_fin_two Matrix.trace_fin_two Matrix.discr_fin_two Iff.not Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul sub_self add_zero zero_sub discrim.eq_1 sq sub_eq_add_neg neg_add_rev neg_neg quadratic_eq_zero_iff_of_discrim_eq_zero map_sub RingHomClass.toAddMonoidHomClass Polynomial.aeval_sub Polynomial.eval_add Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_pow Polynomial.eval_X Polynomial.eval_sub Polynomial.aeval_C

OnePoint

Definitions

Name	Category	Theorems
equivProjectivization 📖	CompOp	4 math math: equivProjectivization_symm_apply_mk, smul_infty_def, equivProjectivization_apply_coe, equivProjectivization_apply_infinity
instGLAction 📖	CompOp	16 math math: isBoundedAt_iff_exists_SL2Z, IsCusp.smul_of_mem, smul_infty_eq_self_iff, isZeroAt_iff_exists_SL2Z, isCusp_SL2Z_iff', smul_some_eq_ite, map_smul, IsZeroAt.smul_iff, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, smul_infty_eq_ite, IsBoundedAt.smul_iff, smul_infty_def, cosetToCuspOrbit_apply_mk, exists_mem_SL2, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff, IsCusp.smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivProjectivization_apply_coe 📖	mathematical	—	DFunLike.coe Equiv OnePoint Projectivization Prod.instAddCommGroup Ring.toAddCommGroup DivisionRing.toRing Prod.instModule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule EquivLike.toFunLike Equiv.instEquivLike equivProjectivization some AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
equivProjectivization_apply_infinity 📖	mathematical	—	DFunLike.coe Equiv OnePoint Projectivization Prod.instAddCommGroup Ring.toAddCommGroup DivisionRing.toRing Prod.instModule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule EquivLike.toFunLike Equiv.instEquivLike equivProjectivization infty AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
equivProjectivization_symm_apply_mk 📖	mathematical	—	DFunLike.coe Equiv Projectivization Prod.instAddCommGroup Ring.toAddCommGroup DivisionRing.toRing Prod.instModule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule OnePoint EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivProjectivization MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass infty some Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	Projectivization.lift.congr_simp
map_smul 📖	mathematical	—	map DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike Matrix.GeneralLinearGroup Fin.fintype OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction instGLAction CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.map	—	smul_infty_eq_ite map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Matrix.GeneralLinearGroup.map_apply IsLocalRing.toNontrivial Field.instIsLocalRing smul_some_eq_ite NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass
smul_infty_def 📖	mathematical	—	Matrix.GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction instGLAction infty DFunLike.coe Equiv Projectivization Field.toDivisionRing Prod.instAddCommGroup Ring.toAddCommGroup DivisionRing.toRing Prod.instModule DivisionRing.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivProjectivization Units.val	—	smul_ne_zero_iff_ne RingHomInvPair.ids LinearEquiv.left_inv LinearEquiv.right_inv Matrix.mulVec_eq_sum Finset.sum_congr IsCentralScalar.op_smul_eq_smul Pi.isCentralScalar CommSemigroup.isCentralScalar Fin.sum_univ_two one_smul Matrix.cons_val_fin_one zero_smul add_zero
smul_infty_eq_ite 📖	mathematical	—	Matrix.GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction instGLAction infty Units.val MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain some DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	smul_infty_def div_eq_inv_mul
smul_infty_eq_self_iff 📖	mathematical	—	Matrix.GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction instGLAction infty Units.val MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	smul_infty_eq_ite
smul_some_eq_ite 📖	mathematical	—	Matrix.GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction instGLAction some Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul Units.val MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass infty DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	smul_ne_zero_iff_ne RingHomInvPair.ids LinearEquiv.left_inv LinearEquiv.right_inv Matrix.mulVec_eq_sum Finset.sum_congr IsCentralScalar.op_smul_eq_smul Pi.isCentralScalar CommSemigroup.isCentralScalar Fin.sum_univ_two Matrix.cons_val_fin_one one_smul mul_comm div_eq_inv_mul

(root)

Definitions

Name	Category	Theorems
instModuleMatrixFinOfNatNatProd 📖	CompOp	3 math math: instSMulCommClassMatrixFinOfNatNatProd, Matrix.fin_two_smul_prod, Matrix.GeneralLinearGroup.fin_two_smul_prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSMulCommClassMatrixFinOfNatNatProd 📖	mathematical	—	SMulCommClass Matrix SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Prod.instAddZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Fin.fintype Prod.instAddMonoid Module.toDistribMulAction Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleMatrixFinOfNatNatProd Prod.instSMul	—	Equiv.smulCommClass RingHomInvPair.ids Matrix.instSMulCommClassForall

---

← Back to Index