Documentation Verification Report

Krasner

📁 Source: Mathlib/Analysis/Normed/Field/Krasner.lean

Statistics

Metric	Count
Definitions `IsKrasner`	1
Theorems `krasner`, `krasner'`, `of_completeSpace`, `of_completeSpace_of_normal`	4
Total	5

IsKrasner

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`krasner` 📖	mathematical	`Polynomial.Separable` `Semifield.toCommSemiring` `Field.toSemifield` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NormedField.toField` `Polynomial.map` `algebraMap` `IsIntegral` `Real` `Real.instLT` `Norm.norm` `NormedField.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing`	`IntermediateField` `NormedField.toField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet`	—	`krasner'`
`krasner'` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly` `IsIntegral` `Real` `Real.instLT` `Norm.norm` `NormedField.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing`	`IntermediateField` `NormedField.toField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet`	—	—
`of_completeSpace` 📖	mathematical	—	`IsKrasner` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toAlgebra` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`AlgebraicClosure.isAlgebraic` `AlgebraicClosure.isAlgClosed` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsScalarTower.of_algHom` `of_completeSpace_of_normal` `IsAlgClosure.normal` `AlgebraicClosure.instIsAlgClosureOfIsAlgebraic` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.isSeparable_self` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `krasner` `Polynomial.Separable.of_dvd` `IsSeparable.map` `RingHom.injective` `DivisionRing.isSimpleRing` `dvd_rfl` `Polynomial.Splits.of_dvd` `Polynomial.Splits.of_isScalarTower` `Polynomial.map_ne_zero` `minpoly.ne_zero` `IsSeparable.isIntegral` `Polynomial.map_dvd` `Polynomial.map_id` `minpoly.dvd_map_of_isScalarTower'` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `IsIntegral.map` `IsScalarTower.left` `AlgHom.algHomClass` `minpoly.algHom_eq` `isConjRoot_iff_mem_minpoly_rootSet` `Polynomial.Splits.image_rootSet` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass`
`of_completeSpace_of_normal` 📖	mathematical	—	`IsKrasner` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAlgebra.toAlgebra` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`IsScalarTower.left` `IntermediateField.adjoin.finiteDimensional` `IsUltrametricDist.of_normedAlgebra` `Field.isSeparable_sub` `IsSeparable.tower_top` `IntermediateField.isScalarTower_mid'` `isSeparable_algebraMap` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `notMem_iff_exists_ne_and_isConjRoot` `minpoly_sub_algebraMap_splits` `IsIntegral.minpoly_splits_tower_top` `IsSeparable.isIntegral` `isConjRoot_iff_exists_algEquiv` `IntermediateField.normal` `sub_eq_add_neg` `norm_neg` `IsUltrametricDist.norm_add_le_max` `NormedAlgebra.norm_eq_spectralNorm` `AlgEquiv.symm_apply_apply` `AlgEquiv.restrictScalars_apply` `spectralNorm_eq_of_equiv` `instReflLe` `IsConjRoot.of_isScalarTower` `instIsDomain` `sub_add_cancel` `IsConjRoot.add_algebraMap` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass`

(root)

Definitions

Name	Category	Theorems
`IsKrasner` 📖	CompData	2 math math: `IsKrasner.of_completeSpace_of_normal`, `IsKrasner.of_completeSpace`

---

← Back to Index