Documentation Verification Report

FiniteDimensional

📁 Source: Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean

Statistics

Metric	Count
Definitions	0
Theorems `finrank_real_complex`, `finrank_real_complex_fact`, `instFiniteDimensionalReal`, `nonempty_linearEquiv_real`, `rank_rat_complex`, `rank_real_complex`, `rank_real_complex'`, `complexToReal`, `rank_rat_real`, `finrank_real_of_complex`, `rank_real_of_complex`	11
Total	11

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_real_complex` 📖	mathematical	—	`Module.finrank` `Real` `Complex` `Real.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Module.complexToReal` `addCommGroup` `Semiring.toModule` `instSemiring`	—	`Module.finrank_eq_card_basis` `IsNoetherianRing.strongRankCondition` `Real.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Fintype.card_fin`
`finrank_real_complex_fact` 📖	mathematical	—	`Fact` `Module.finrank` `Real` `Complex` `Real.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Module.complexToReal` `addCommGroup` `Semiring.toModule` `instSemiring`	—	`finrank_real_complex`
`instFiniteDimensionalReal` 📖	mathematical	—	`FiniteDimensional` `Real` `Complex` `Real.instDivisionRing` `addCommGroup` `Module.complexToReal` `Semiring.toModule` `instSemiring`	—	`Module.Basis.finiteDimensional_of_finite` `Finite.of_fintype`
`nonempty_linearEquiv_real` 📖	mathematical	—	`LinearEquiv` `Rat.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Complex` `Real` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Real.instAddCommMonoid` `Algebra.toModule` `Rat.commSemiring` `instSemiring` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `instField` `instCharZero` `Real.semiring` `Real.instDivisionRing` `IsStrictOrderedRing.toCharZero` `Ring.toSemiring` `DivisionRing.toRing` `Real.partialOrder` `Real.instIsStrictOrderedRing`	—	`RingHomInvPair.ids` `instCharZero` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `LinearEquiv.nonempty_equiv_iff_rank_eq` `IsNoetherianRing.strongRankCondition` `Rat.nontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Module.Free.of_divisionRing` `rank_rat_complex` `Real.rank_rat_real`
`rank_rat_complex` 📖	mathematical	—	`Module.rank` `Complex` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Algebra.toModule` `Rat.commSemiring` `instSemiring` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `instField` `instCharZero` `Cardinal.continuum`	—	`instCharZero` `Module.Free.rank_eq_mk_of_infinite_lt` `IsNoetherianRing.strongRankCondition` `Rat.nontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Module.Free.of_divisionRing` `NoMinOrder.infinite` `instNoMinOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Cardinal.mk_eq_aleph0` `Encodable.countable` `Cardinal.lift_id` `Cardinal.mk_complex` `Cardinal.aleph0_lt_continuum`
`rank_real_complex` 📖	mathematical	—	`Module.rank` `Real` `Complex` `Real.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Module.complexToReal` `addCommGroup` `Semiring.toModule` `instSemiring` `Cardinal` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `IsNoetherianRing.strongRankCondition` `Real.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `instFiniteDimensionalReal` `finrank_real_complex`
`rank_real_complex'` 📖	mathematical	—	`Cardinal.lift` `Module.rank` `Real` `Complex` `Real.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Module.complexToReal` `addCommGroup` `Semiring.toModule` `instSemiring` `Cardinal` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Module.finrank_eq_rank` `IsNoetherianRing.strongRankCondition` `Real.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `instFiniteDimensionalReal` `finrank_real_complex` `Cardinal.lift_natCast` `Nat.cast_ofNat`

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complexToReal` 📖	mathematical	—	`FiniteDimensional` `Real` `Real.instDivisionRing` `Module.complexToReal`	—	`trans` `IsScalarTower.complexToReal` `IsScalarTower.left` `Complex.instFiniteDimensionalReal`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rank_rat_real` 📖	mathematical	—	`Module.rank` `Real` `Rat.semiring` `instAddCommMonoid` `Algebra.toModule` `Rat.commSemiring` `semiring` `DivisionRing.toRatAlgebra` `instDivisionRing` `IsStrictOrderedRing.toCharZero` `Ring.toSemiring` `DivisionRing.toRing` `partialOrder` `instIsStrictOrderedRing` `Cardinal.continuum`	—	`IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Module.Free.rank_eq_mk_of_infinite_lt` `IsNoetherianRing.strongRankCondition` `Rat.nontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Module.Free.of_divisionRing` `NoMinOrder.infinite` `instNoMinOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Cardinal.mk_eq_aleph0` `Encodable.countable` `Cardinal.lift_id` `Cardinal.mk_real` `Cardinal.aleph0_lt_continuum`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_real_of_complex` 📖	mathematical	—	`Module.finrank` `Real` `Real.semiring` `AddCommGroup.toAddCommMonoid` `Module.complexToReal` `Complex` `Complex.instSemiring`	—	`Module.finrank_mul_finrank` `IsScalarTower.complexToReal` `IsScalarTower.left` `IsNoetherianRing.strongRankCondition` `Real.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Complex.instNontrivial` `Module.Free.of_divisionRing` `Complex.finrank_real_complex`
`rank_real_of_complex` 📖	mathematical	—	`Module.rank` `Real` `Real.semiring` `AddCommGroup.toAddCommMonoid` `Module.complexToReal` `Cardinal` `Cardinal.instMul` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex` `Complex.instSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `lift_rank_mul_lift_rank` `IsScalarTower.complexToReal` `IsScalarTower.left` `IsNoetherianRing.strongRankCondition` `Real.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Complex.instNontrivial` `Module.Free.of_divisionRing` `Complex.rank_real_complex'` `Cardinal.lift_id'`

---

← Back to Index