linter

src/analysis/calculus/iterated_deriv_mathlib.lean

@@ -1,45 +1,12 @@
 /-
-Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
+Copyright (c) 2023 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel
+Authors: Bhavik Mehta
 -/
 import analysis.calculus.iterated_deriv
 
 /-!
-# One-dimensional iterated derivatives
-
-> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-> Any changes to this file require a corresponding PR to mathlib4.
-
-We define the `n`-th derivative of a function `f : 𝕜 → F` as a function
-`iterated_deriv n f : 𝕜 → F`, as well as a version on domains `iterated_deriv_within n f s : 𝕜 → F`,
-and prove their basic properties.
-
-## Main definitions and results
-
-Let `𝕜` be a nontrivially normed field, and `F` a normed vector space over `𝕜`. Let `f : 𝕜 → F`.
-
-* `iterated_deriv n f` is the `n`-th derivative of `f`, seen as a function from `𝕜` to `F`.
-  It is defined as the `n`-th Fréchet derivative (which is a multilinear map) applied to the
-  vector `(1, ..., 1)`, to take advantage of all the existing framework, but we show that it
-  coincides with the naive iterative definition.
-* `iterated_deriv_eq_iterate` states that the `n`-th derivative of `f` is obtained by starting
-  from `f` and differentiating it `n` times.
-* `iterated_deriv_within n f s` is the `n`-th derivative of `f` within the domain `s`. It only
-  behaves well when `s` has the unique derivative property.
-* `iterated_deriv_within_eq_iterate` states that the `n`-th derivative of `f` in the domain `s` is
-  obtained by starting from `f` and differentiating it `n` times within `s`. This only holds when
-  `s` has the unique derivative property.
-
-## Implementation details
-
-The results are deduced from the corresponding results for the more general (multilinear) iterated
-Fréchet derivative. For this, we write `iterated_deriv n f` as the composition of
-`iterated_fderiv 𝕜 n f` and a continuous linear equiv. As continuous linear equivs respect
-differentiability and commute with differentiation, this makes it possible to prove readily that
-the derivative of the `n`-th derivative is the `n+1`-th derivative in `iterated_deriv_within_succ`,
-by translating the corresponding result `iterated_fderiv_within_succ_apply_left` for the
-iterated Fréchet derivative.
+# Stuff for analysis.calculus.iterated_deriv
 -/
 
 noncomputable theory

src/analysis/calculus/taylor_mathlib.lean

@@ -1,7 +1,16 @@
+/-
+Copyright (c) 2023 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
 import analysis.calculus.taylor
 import analysis.calculus.cont_diff
 import data.set.intervals.unordered_interval
 
+/-!
+# Stuff for analysis.calculus.taylor
+-/
+
 open set
 
 open_locale nat

src/combinatorics/simple_graph/clique_mathlib.lean

@@ -1,6 +1,15 @@
+/-
+Copyright (c) 2023 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
 import combinatorics.simple_graph.basic_mathlib
 import combinatorics.simple_graph.clique
 
+/-!
+# Stuff for combinatorics.simple_graph.clique
+-/
+
 namespace simple_graph
 
 variables {V W : Type*} {G : simple_graph V} {H : simple_graph W} {n : ℕ}

src/data/fin/vec_notation_mathlib.lean

@@ -1,5 +1,14 @@
+/-
+Copyright (c) 2023 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
 import data.fin.vec_notation
 
+/-!
+# Stuff for data.fin.vec_notation
+-/
+
 namespace function
 open matrix (vec_cons)
 open fin

src/number_theory/legendre_symbol/quadratic_char/basic_mathlib.lean

@@ -1,6 +1,15 @@
+/-
+Copyright (c) 2023 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
 import data.fintype.parity
 import number_theory.legendre_symbol.quadratic_char.basic
 
+/-!
+# Stuff for number_theory.legendre_symbol.quadratic_char.basic
+-/
+
 open fintype (card)
 open finset