From b1c827ee4f94d72fce1db4051be918c2e521711a Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 20 Nov 2024 07:41:46 +0100 Subject: [PATCH] de-googlify IARC committee for copyright waiver has been granted, so we remove CLA bot and change copyright headers. --- CONTRIBUTING.md | 12 ------------ FormalBook/Chapter_01.lean | 16 ++-------------- FormalBook/Chapter_02.lean | 16 ++-------------- FormalBook/Chapter_03.lean | 16 ++-------------- FormalBook/Chapter_04.lean | 16 ++-------------- FormalBook/Chapter_05.lean | 16 ++-------------- FormalBook/Chapter_06.lean | 16 ++-------------- FormalBook/Chapter_07.lean | 16 ++-------------- FormalBook/Chapter_08.lean | 16 ++-------------- FormalBook/Chapter_09.lean | 16 ++-------------- FormalBook/Chapter_10.lean | 16 ++-------------- FormalBook/Chapter_11.lean | 18 ++---------------- FormalBook/Chapter_12.lean | 16 ++-------------- FormalBook/Chapter_13.lean | 16 ++-------------- FormalBook/Chapter_14.lean | 16 ++-------------- FormalBook/Chapter_15.lean | 16 ++-------------- FormalBook/Chapter_16.lean | 16 ++-------------- FormalBook/Chapter_17.lean | 16 ++-------------- FormalBook/Chapter_18.lean | 16 ++-------------- FormalBook/Chapter_19.lean | 16 ++-------------- FormalBook/Chapter_20.lean | 16 ++-------------- FormalBook/Chapter_21.lean | 16 ++-------------- FormalBook/Chapter_22.lean | 16 ++-------------- FormalBook/Chapter_23.lean | 16 ++-------------- FormalBook/Chapter_24.lean | 16 ++-------------- FormalBook/Chapter_25.lean | 16 ++-------------- FormalBook/Chapter_26.lean | 16 ++-------------- FormalBook/Chapter_27.lean | 16 ++-------------- FormalBook/Chapter_28.lean | 16 ++-------------- FormalBook/Chapter_29.lean | 16 ++-------------- FormalBook/Chapter_30.lean | 16 ++-------------- FormalBook/Chapter_31.lean | 16 ++-------------- FormalBook/Chapter_32.lean | 16 ++-------------- FormalBook/Chapter_33.lean | 16 ++-------------- FormalBook/Chapter_34.lean | 16 ++-------------- FormalBook/Chapter_35.lean | 16 ++-------------- FormalBook/Chapter_36.lean | 16 ++-------------- FormalBook/Chapter_37.lean | 16 ++-------------- FormalBook/Chapter_38.lean | 16 ++-------------- FormalBook/Chapter_39.lean | 16 ++-------------- FormalBook/Chapter_40.lean | 16 ++-------------- FormalBook/Chapter_41.lean | 16 ++-------------- FormalBook/Chapter_42.lean | 16 ++-------------- FormalBook/Chapter_43.lean | 16 ++-------------- FormalBook/Chapter_44.lean | 16 ++-------------- FormalBook/Chapter_45.lean | 16 ++-------------- README.md | 8 +------- 47 files changed, 91 insertions(+), 651 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 6272489..fd73c2d 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -3,18 +3,6 @@ We'd love to accept your patches and contributions to this project. There are just a few small guidelines you need to follow. -## Contributor License Agreement - -Contributions to this project must be accompanied by a Contributor License -Agreement. You (or your employer) retain the copyright to your contribution; -this simply gives us permission to use and redistribute your contributions as -part of the project. Head over to to see -your current agreements on file or to sign a new one. - -You generally only need to submit a CLA once, so if you've already submitted one -(even if it was for a different project), you probably don't need to do it -again. - ## Code Reviews All submissions, including submissions by project members, require review. We diff --git a/FormalBook/Chapter_01.lean b/FormalBook/Chapter_01.lean index baa416d..fa9c395 100644 --- a/FormalBook/Chapter_01.lean +++ b/FormalBook/Chapter_01.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching, Ralf Stephan -/ import Mathlib.NumberTheory.LucasLehmer diff --git a/FormalBook/Chapter_02.lean b/FormalBook/Chapter_02.lean index 3cd921d..e837df9 100644 --- a/FormalBook/Chapter_02.lean +++ b/FormalBook/Chapter_02.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Analysis.Convex.SpecificFunctions.Basic diff --git a/FormalBook/Chapter_03.lean b/FormalBook/Chapter_03.lean index 3e83d07..e22bd3d 100644 --- a/FormalBook/Chapter_03.lean +++ b/FormalBook/Chapter_03.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching, Christopher Schmidt -/ import Mathlib.Analysis.Normed.Field.Lemmas diff --git a/FormalBook/Chapter_04.lean b/FormalBook/Chapter_04.lean index e6e145e..837b9ab 100644 --- a/FormalBook/Chapter_04.lean +++ b/FormalBook/Chapter_04.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_05.lean b/FormalBook/Chapter_05.lean index 4952ada..8403fcf 100644 --- a/FormalBook/Chapter_05.lean +++ b/FormalBook/Chapter_05.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching, Nikolas Kuhn -/ import Mathlib.Algebra.Polynomial.Basic diff --git a/FormalBook/Chapter_06.lean b/FormalBook/Chapter_06.lean index 47562ed..75848be 100644 --- a/FormalBook/Chapter_06.lean +++ b/FormalBook/Chapter_06.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching, Nick Kuhn -/ import Mathlib.RingTheory.Henselian diff --git a/FormalBook/Chapter_07.lean b/FormalBook/Chapter_07.lean index c86ad42..ea83a27 100644 --- a/FormalBook/Chapter_07.lean +++ b/FormalBook/Chapter_07.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_08.lean b/FormalBook/Chapter_08.lean index a7c5238..2071efe 100644 --- a/FormalBook/Chapter_08.lean +++ b/FormalBook/Chapter_08.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_09.lean b/FormalBook/Chapter_09.lean index 3e0b2ea..aa62cf6 100644 --- a/FormalBook/Chapter_09.lean +++ b/FormalBook/Chapter_09.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_10.lean b/FormalBook/Chapter_10.lean index 35a2230..c4287e9 100644 --- a/FormalBook/Chapter_10.lean +++ b/FormalBook/Chapter_10.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_11.lean b/FormalBook/Chapter_11.lean index 48046a6..33c8e6d 100644 --- a/FormalBook/Chapter_11.lean +++ b/FormalBook/Chapter_11.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic @@ -33,5 +21,3 @@ import Mathlib.Tactic - proof Appendix: Basic graph concepts -/ - - diff --git a/FormalBook/Chapter_12.lean b/FormalBook/Chapter_12.lean index 217dfdb..6f1d6fb 100644 --- a/FormalBook/Chapter_12.lean +++ b/FormalBook/Chapter_12.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_13.lean b/FormalBook/Chapter_13.lean index bf2b949..03a242b 100644 --- a/FormalBook/Chapter_13.lean +++ b/FormalBook/Chapter_13.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_14.lean b/FormalBook/Chapter_14.lean index 14a9f9b..9deb44d 100644 --- a/FormalBook/Chapter_14.lean +++ b/FormalBook/Chapter_14.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_15.lean b/FormalBook/Chapter_15.lean index 6f9c716..f9de2cb 100644 --- a/FormalBook/Chapter_15.lean +++ b/FormalBook/Chapter_15.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_16.lean b/FormalBook/Chapter_16.lean index d86a1fa..3f76c92 100644 --- a/FormalBook/Chapter_16.lean +++ b/FormalBook/Chapter_16.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_17.lean b/FormalBook/Chapter_17.lean index 018a046..63409e8 100644 --- a/FormalBook/Chapter_17.lean +++ b/FormalBook/Chapter_17.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_18.lean b/FormalBook/Chapter_18.lean index f12df59..958bbaf 100644 --- a/FormalBook/Chapter_18.lean +++ b/FormalBook/Chapter_18.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_19.lean b/FormalBook/Chapter_19.lean index 762ac5f..3ba9cc3 100644 --- a/FormalBook/Chapter_19.lean +++ b/FormalBook/Chapter_19.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_20.lean b/FormalBook/Chapter_20.lean index 6b666a2..acd88b6 100644 --- a/FormalBook/Chapter_20.lean +++ b/FormalBook/Chapter_20.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Analysis.InnerProductSpace.Basic diff --git a/FormalBook/Chapter_21.lean b/FormalBook/Chapter_21.lean index 4514adc..f0d3134 100644 --- a/FormalBook/Chapter_21.lean +++ b/FormalBook/Chapter_21.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_22.lean b/FormalBook/Chapter_22.lean index ffb575d..2c2bfdf 100644 --- a/FormalBook/Chapter_22.lean +++ b/FormalBook/Chapter_22.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_23.lean b/FormalBook/Chapter_23.lean index f626468..5a7da50 100644 --- a/FormalBook/Chapter_23.lean +++ b/FormalBook/Chapter_23.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_24.lean b/FormalBook/Chapter_24.lean index 717d909..0fc096e 100644 --- a/FormalBook/Chapter_24.lean +++ b/FormalBook/Chapter_24.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Data.Matrix.DoublyStochastic diff --git a/FormalBook/Chapter_25.lean b/FormalBook/Chapter_25.lean index 9d11ed5..9fcbe90 100644 --- a/FormalBook/Chapter_25.lean +++ b/FormalBook/Chapter_25.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_26.lean b/FormalBook/Chapter_26.lean index 17a5bf4..359b657 100644 --- a/FormalBook/Chapter_26.lean +++ b/FormalBook/Chapter_26.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_27.lean b/FormalBook/Chapter_27.lean index 4e71fe3..e136079 100644 --- a/FormalBook/Chapter_27.lean +++ b/FormalBook/Chapter_27.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_28.lean b/FormalBook/Chapter_28.lean index bc6eda1..e011f02 100644 --- a/FormalBook/Chapter_28.lean +++ b/FormalBook/Chapter_28.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_29.lean b/FormalBook/Chapter_29.lean index dcb3458..7146cfe 100644 --- a/FormalBook/Chapter_29.lean +++ b/FormalBook/Chapter_29.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_30.lean b/FormalBook/Chapter_30.lean index 597076f..bd39b4d 100644 --- a/FormalBook/Chapter_30.lean +++ b/FormalBook/Chapter_30.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_31.lean b/FormalBook/Chapter_31.lean index 05c5cf9..ea3ee54 100644 --- a/FormalBook/Chapter_31.lean +++ b/FormalBook/Chapter_31.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_32.lean b/FormalBook/Chapter_32.lean index 737cda4..5b288e6 100644 --- a/FormalBook/Chapter_32.lean +++ b/FormalBook/Chapter_32.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching, Christopher Schmidt -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_33.lean b/FormalBook/Chapter_33.lean index 172b332..83ad40f 100644 --- a/FormalBook/Chapter_33.lean +++ b/FormalBook/Chapter_33.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_34.lean b/FormalBook/Chapter_34.lean index a32bd56..affa29c 100644 --- a/FormalBook/Chapter_34.lean +++ b/FormalBook/Chapter_34.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_35.lean b/FormalBook/Chapter_35.lean index e9f625d..24afef6 100644 --- a/FormalBook/Chapter_35.lean +++ b/FormalBook/Chapter_35.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_36.lean b/FormalBook/Chapter_36.lean index afc9b45..7ce0529 100644 --- a/FormalBook/Chapter_36.lean +++ b/FormalBook/Chapter_36.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_37.lean b/FormalBook/Chapter_37.lean index e8b37ec..fa45878 100644 --- a/FormalBook/Chapter_37.lean +++ b/FormalBook/Chapter_37.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_38.lean b/FormalBook/Chapter_38.lean index 74c00da..6845730 100644 --- a/FormalBook/Chapter_38.lean +++ b/FormalBook/Chapter_38.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_39.lean b/FormalBook/Chapter_39.lean index fecea04..be6c356 100644 --- a/FormalBook/Chapter_39.lean +++ b/FormalBook/Chapter_39.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_40.lean b/FormalBook/Chapter_40.lean index f493179..cb344bb 100644 --- a/FormalBook/Chapter_40.lean +++ b/FormalBook/Chapter_40.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_41.lean b/FormalBook/Chapter_41.lean index ed876c0..5116c5c 100644 --- a/FormalBook/Chapter_41.lean +++ b/FormalBook/Chapter_41.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_42.lean b/FormalBook/Chapter_42.lean index 5dbbc55..b4db5b6 100644 --- a/FormalBook/Chapter_42.lean +++ b/FormalBook/Chapter_42.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_43.lean b/FormalBook/Chapter_43.lean index 6e050b0..c3b37d3 100644 --- a/FormalBook/Chapter_43.lean +++ b/FormalBook/Chapter_43.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_44.lean b/FormalBook/Chapter_44.lean index 73286af..e7298f1 100644 --- a/FormalBook/Chapter_44.lean +++ b/FormalBook/Chapter_44.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Tactic diff --git a/FormalBook/Chapter_45.lean b/FormalBook/Chapter_45.lean index 5330d1f..5f5a033 100644 --- a/FormalBook/Chapter_45.lean +++ b/FormalBook/Chapter_45.lean @@ -1,18 +1,6 @@ /- -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. - +Copyright 2022 Moritz Firsching. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. Authors: Moritz Firsching -/ import Mathlib.Combinatorics.SimpleGraph.Maps diff --git a/README.md b/README.md index 3006d25..2c7d4e7 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ # Formal BOOK > 🚀 **Pull Requests Welcome!** 🎉 -> +> > We warmly welcome contributions from everyone. > No experience is necessary, and partial proofs help with LaTex are appreciated! @@ -63,9 +63,3 @@ which also has a nice [blog](https://thebook.zib.de/) on the proofs formalized t ## License Apache 2.0; see [`LICENSE`](LICENSE) for details. - -## Disclaimer - -This project is not an official Google project. It is not supported by -Google and Google specifically disclaims all warranties as to its quality, -merchantability, or fitness for a particular purpose.