feat: Valuative criterion for properness. #62991
Annotations
7 errors
|
lint:
Mathlib/ValuativeCriterion/Fiber.lean#L4
Mathlib/ValuativeCriterion/Fiber.lean:4 ERR_MOD: Module docstring missing, or too late
|
|
lint:
Mathlib/ValuativeCriterion/Immersion.lean#L10
Mathlib/ValuativeCriterion/Immersion.lean:10 ERR_MOD: Module docstring missing, or too late
|
|
lint:
Mathlib/ValuativeCriterion/Lemmas.lean#L3
Mathlib/ValuativeCriterion/Lemmas.lean:3 ERR_MOD: Module docstring missing, or too late
|
|
lint:
Mathlib/ValuativeCriterion/UniversallyClosed.lean#L7
Mathlib/ValuativeCriterion/UniversallyClosed.lean:7 ERR_MOD: Module docstring missing, or too late
|
|
lint:
Mathlib/ValuativeCriterion/ValuationRing.lean#L26
Mathlib/ValuativeCriterion/ValuationRing.lean:26 ERR_IND: If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)
|
|
lint:
Mathlib/ValuativeCriterion/ValuationRing.lean#L3
Mathlib/ValuativeCriterion/ValuationRing.lean:3 ERR_MOD: Module docstring missing, or too late
|
|
lint:
Mathlib/ValuativeCriterion/ValuativeCriterion.lean#L7
Mathlib/ValuativeCriterion/ValuativeCriterion.lean:7 ERR_MOD: Module docstring missing, or too late
|
Loading