Skip to content
bot fix style (comment)

[Merged by Bors] - chore: avoid some (0 < ((↑) : ℝ≥0 → ℝ) x) = (0 < x) defeq abuses #7628

Sign in to view logs

[Merged by Bors] - chore: avoid some (0 < ((↑) : ℝ≥0 → ℝ) x) = (0 < x) defeq abuses

[Merged by Bors] - chore: avoid some (0 < ((↑) : ℝ≥0 → ℝ) x) = (0 < x) defeq abuses #7628

Triggered via issue October 19, 2024 23:14
@FR-vdash-botFR-vdash-bot
commented on #17946 e0dccaa
Status Skipped
Total duration 2s
Artifacts –

bot_fix_style_comment.yaml

on: issue_comment
Fix style issues from lint
0s
Fix style issues from lint
Fit to window
Zoom out
Zoom in