lint and suggest

feat(Analysis/InnerProductSpace/Dual, Mathlib/Analysis/Normed/Group/SeparationQuotient): add null submodule and various lifts #61794

Sign in to view logs

Triggered via pull request October 22, 2024 09:52

synchronize #16707

yoh-tanimoto-innerproductspace-quotient

Status Success

Total duration 1m 29s

Artifacts –

lint_and_suggest_pr.yml

on: pull_request

Check all files imported