Commit 2024-10-24 19:28 779f4ef1

chore: make the model with corners implicit in differential geometry statements (#17687) Currently, the model with corners I is explicit in many (most?) differential geometry statements. However, when rewriting, or applying theorems, it can be inferred from the context 95% of the time. Therefore, we make it implicit in most statements: the rule of thumb is that in variable lines we should have {I : ModelWithCorners 𝕜 E H}, and use variable (I) in for definitions. This looks like a clear improvement to me, making proofs more readable and avoiding clutter. For the few cases where we need to provide it explicitly, named arguments work well. No mathematical change at all, just arguments implicitness.