GelfandMazur

📁 Source: Mathlib/Analysis/Normed/Algebra/GelfandMazur.lean

Statistics

Metric	Count
Definitions algEquivOfNormMul	1
Theorems exists_norm_sub_smul_one_eq_zero, nonempty_algEquiv, exists_isMonicOfDegree_two_and_aeval_eq_zero, nonempty_algEquiv_or, exists_isMinOn_norm_sub_smul	5
Total	6

NormedAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isMinOn_norm_sub_smul 📖	mathematical	—	IsMinOn Real Real.instPreorder Norm.norm SeminormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField Ring.toSemiring SeminormedRing.toRing RingHom.instFunLike algebraMap toAlgebra Set.univ	—	Filter.Tendsto.comp tendsto_norm_cobounded_atTop tendsto_const_sub_cobounded Continuous.exists_forall_le_of_isBounded HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Continuous.norm Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_const continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass sub_zero zero_smul Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial

NormedAlgebra.Complex

Definitions

Name	Category	Theorems
algEquivOfNormMul 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_norm_sub_smul_one_eq_zero 📖	mathematical	—	Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring Ring.toSemiring NormedRing.toRing RingHom.instFunLike algebraMap NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing Real Real.instZero	—	NormedAlgebra.exists_isMinOn_norm_sub_smul Complex.instProperSpace eq_or_lt_of_le norm_nonneg LE.le.trans_eq norm_sub_norm_le norm_sub_rev Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_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.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono le_of_lt add_pos' Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Real.norm_eq_abs Complex.norm_real mul_one NormOneClass.norm_one norm_algebraMap
nonempty_algEquiv 📖	mathematical	—	AlgEquiv Complex Complex.instCommSemiring Complex.instSemiring Ring.toSemiring NormedRing.toRing Algebra.id NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing	—	—

NormedAlgebra.Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isMonicOfDegree_two_and_aeval_eq_zero 📖	mathematical	—	Polynomial.IsMonicOfDegree Real Real.semiring DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Real.instCommSemiring Polynomial.semiring Ring.toSemiring NormedRing.toRing Polynomial.algebraOfAlgebra Algebra.id NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	sq_le_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing Real.sqrt_nonneg norm_nonneg Real.sq_sqrt norm_pow Nat.instAtLeastTwoHAddOfNat Commute.sub_sq Algebra.commute_algebraMap_right Algebra.algebraMap_eq_smul_one two_mul mul_add Distrib.leftDistribClass Algebra.smul_def map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass add_mul Distrib.rightDistribClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass isMinOn_univ_iff tendsto_norm_atTop_iff_cobounded Real.sqrt_pos_of_pos norm_pos_iff Filter.not_tendsto_const_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instNontrivial RealNormedSpace.cobounded_neBot nontrivial_prod_left norm_ne_zero_iff Polynomial.isMonicOfDegree_sub_add_two
nonempty_algEquiv_or 📖	mathematical	—	AlgEquiv Real Real.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Real.semiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Algebra.id Complex Complex.instSemiring Complex.instNormedField RCLike.toNormedAlgebra Complex.instRCLike	—	exists_isMonicOfDegree_two_and_aeval_eq_zero NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Polynomial.IsMonicOfDegree.ne_zero Real.instNontrivial Real.nonempty_algEquiv_or

---

← Back to Index