Documentation Verification Report

Projectivization

📁 Source: Mathlib/NumberTheory/Height/Projectivization.lean

Statistics

Metric	Count
Definitions `evalProjLogHeight`, `evalProjMulHeight`, `Projectivization`, `logHeight`, `mulHeight`	5
Theorems `logHeight_eq_log_mulHeight`, `logHeight_mk`, `logHeight_nonneg`, `mulHeight_mk`, `mulHeight_ne_zero`, `mulHeight_pos`, `one_le_mulHeight`	7
Total	12

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalProjLogHeight` 📖	CompOp	—
`evalProjMulHeight` 📖	CompOp	—

Projectivization

Definitions

Name	Category	Theorems
`logHeight` 📖	CompOp	3 math math: `logHeight_nonneg`, `logHeight_eq_log_mulHeight`, `logHeight_mk`
`mulHeight` 📖	CompOp	4 math math: `mulHeight_mk`, `mulHeight_pos`, `logHeight_eq_log_mulHeight`, `one_le_mulHeight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`logHeight_eq_log_mulHeight` 📖	mathematical	—	`logHeight` `Real.log` `mulHeight`	—	`rep_nonzero` `mk_rep` `Height.logHeight.eq_1`
`logHeight_mk` 📖	mathematical	—	`logHeight` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `Height.logHeight`	—	—
`logHeight_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `logHeight`	—	`logHeight_eq_log_mulHeight` `Real.log_nonneg` `one_le_mulHeight`
`mulHeight_mk` 📖	mathematical	—	`mulHeight` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `Height.mulHeight`	—	—
`mulHeight_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `mulHeight_pos`
`mulHeight_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `mulHeight`	—	`LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `one_le_mulHeight`
`one_le_mulHeight` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `mulHeight`	—	`rep_nonzero` `mk_rep` `Height.one_le_mulHeight`

(root)

Definitions

Name	Category	Theorems
`Projectivization` 📖	CompOp	50 math math: `Projectivization.Subspace.mem_add'`, `Projectivization.dependent_pair_iff_eq`, `Projectivization.map_id`, `Projectivization.Subspace.span_sup`, `Projectivization.Subspace.subset_span_trans`, `Projectivization.card''`, `Projectivization.Subspace.span_empty`, `Projectivization.Subspace.span_coe`, `Projectivization.exists_not_orthogonal_self`, `Submodule.mk_mem_projectivization_iff`, `Projectivization.finite_of_finite`, `Projectivization.exists_not_self_orthogonal`, `Projectivization.isEmpty_of_subsingleton`, `Projectivization.finite_iff_of_finite`, `Projectivization.submodule_injective`, `Projectivization.card`, `Configuration.ofField.instNondegenerateProjectivizationForallFinOfNatNat`, `OnePoint.equivProjectivization_symm_apply_mk`, `Projectivization.Subspace.subset_span`, `Projectivization.independent_pair_iff_ne`, `Projectivization.map_injective`, `Submodule.mem_projectivization_iff_submodule_le`, `Projectivization.card_of_finrank`, `Projectivization.Subspace.sup_span`, `Projectivization.Subspace.monotone_span`, `Projectivization.cross_mk`, `Projectivization.dependent_iff`, `Projectivization.card'`, `Projectivization.Subspace.span_le_subspace_iff`, `Projectivization.smul_def`, `Projectivization.map_comp`, `OnePoint.smul_infty_def`, `Projectivization.Subspace.mem_span`, `Projectivization.cross_mk_of_ne`, `Projectivization.Subspace.span_union`, `Projectivization.Subspace.mem_add`, `Projectivization.generalLinearGroup_smul_def`, `Projectivization.Subspace.span_univ`, `Projectivization.card_of_finrank_two`, `OnePoint.equivProjectivization_apply_coe`, `Configuration.ofField.mem_iff`, `Projectivization.instNonemptyOfNontrivial`, `Projectivization.independent_iff`, `Projectivization.Subspace.span_eq_span_iff`, `Projectivization.Subspace.mem_carrier_iff`, `Projectivization.Subspace.span_eq_sInf`, `Projectivization.smul_mk`, `Projectivization.Subspace.span_iUnion`, `Projectivization.Subspace.mem_submodule_iff`, `OnePoint.equivProjectivization_apply_infinity`

---

← Back to Index