Skip to content
Back to pull request #14782

feat: Valuative criterion for properness. #62991

Sign in to view logs

feat: Valuative criterion for properness.

feat: Valuative criterion for properness. #62991

Triggered via pull request October 27, 2024 07:41
@erdOneerdOne
synchronize #14782
valuativeCriterion
Status Success
Total duration 1m 7s
Artifacts –

lint_and_suggest_pr.yml

on: pull_request
Lint style
59s
Lint style
Check all files imported
38s
Check all files imported
Fit to window
Zoom out
Zoom in

Annotations

7 errors
Lint style: Mathlib/ValuativeCriterion/Fiber.lean#L4
Mathlib/ValuativeCriterion/Fiber.lean:4 ERR_MOD: Module docstring missing, or too late
Lint style: Mathlib/ValuativeCriterion/Immersion.lean#L10
Mathlib/ValuativeCriterion/Immersion.lean:10 ERR_MOD: Module docstring missing, or too late
Lint style: Mathlib/ValuativeCriterion/Lemmas.lean#L3
Mathlib/ValuativeCriterion/Lemmas.lean:3 ERR_MOD: Module docstring missing, or too late
Lint style: Mathlib/ValuativeCriterion/UniversallyClosed.lean#L7
Mathlib/ValuativeCriterion/UniversallyClosed.lean:7 ERR_MOD: Module docstring missing, or too late
Lint style: 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 style: Mathlib/ValuativeCriterion/ValuationRing.lean#L3
Mathlib/ValuativeCriterion/ValuationRing.lean:3 ERR_MOD: Module docstring missing, or too late
Lint style: Mathlib/ValuativeCriterion/ValuativeCriterion.lean#L7
Mathlib/ValuativeCriterion/ValuativeCriterion.lean:7 ERR_MOD: Module docstring missing, or too late