Documentation Verification Report

Basic

📁 Source: Mathlib/FieldTheory/IsRealClosed/Basic.lean

Statistics

Metric	Count
Definitions `IsRealClosed`	1
Theorems `exists_eq_pow_of_isSquare`, `exists_eq_pow_of_nonneg`, `exists_eq_pow_of_odd`, `exists_eq_zpow_of_isSquare`, `exists_eq_zpow_of_nonneg`, `exists_eq_zpow_of_odd`, `exists_isRoot_of_odd_natDegree`, `isSquare_neg_of_not_isSquare`, `isSquare_or_isSquare_neg`, `nonneg_iff_isSquare`, `of_linearOrderedField`, `toIsSemireal`, `of_nonneg`, `of_not_isSquare_neg`	14
Total	15

IsRealClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_pow_of_isSquare` 📖	mathematical	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Nat.strong_induction_on` `Nat.even_or_odd` `isSquare_or_isSquare_neg` `pow_add` `mul_neg` `neg_mul` `neg_neg` `exists_eq_pow_of_odd`
`exists_eq_pow_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`exists_eq_pow_of_isSquare` `IsSquare.of_nonneg`
`exists_eq_pow_of_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`exists_isRoot_of_odd_natDegree` `Polynomial.natDegree_sub_C` `Polynomial.natDegree_pow` `IsDomain.to_noZeroDivisors` `Field.isDomain` `Polynomial.natDegree_X` `instNontrivialOfCharZero` `instCharZeroOfIsSemireal` `toIsSemireal` `mul_one` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Polynomial.eval_sub` `Polynomial.eval_pow` `Polynomial.eval_X` `Polynomial.eval_C` `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.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `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.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_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_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero`
`exists_eq_zpow_of_isSquare` 📖	mathematical	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`zpow_natCast` `exists_eq_pow_of_isSquare` `zpow_neg` `inv_pow` `inv_inv`
`exists_eq_zpow_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`exists_eq_zpow_of_isSquare` `IsSquare.of_nonneg`
`exists_eq_zpow_of_odd` 📖	mathematical	`Odd` `Int.instSemiring`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`zpow_natCast` `exists_eq_pow_of_odd` `zpow_neg` `inv_pow` `inv_inv`
`exists_isRoot_of_odd_natDegree` 📖	mathematical	`Odd` `Nat.instSemiring` `Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Polynomial.IsRoot`	—	—
`isSquare_neg_of_not_isSquare` 📖	mathematical	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`isSquare_or_isSquare_neg`
`isSquare_or_isSquare_neg` 📖	mathematical	—	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	—
`nonneg_iff_isSquare` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`le_antisymm` `nonpos_of_neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsSquare.nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `isSquare_or_isSquare_neg`
`of_linearOrderedField` 📖	mathematical	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Polynomial.IsRoot` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`IsRealClosed`	—	`instIsSemirealOfIsStrictOrderedRingOfExistsAddOfLE` `AddGroup.existsAddOfLE` `le_total` `neg_nonneg_of_nonpos` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`toIsSemireal` 📖	mathematical	—	`IsSemireal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—

IsSquare

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsRealClosed.nonneg_iff_isSquare`
`of_not_isSquare_neg` 📖	—	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	—	`IsRealClosed.isSquare_or_isSquare_neg`

(root)

Definitions

Name	Category	Theorems
`IsRealClosed` 📖	CompData	1 math math: `IsRealClosed.of_linearOrderedField`

---

← Back to Index