Search.setIndex({"docnames": ["C01_Introduction", "C02_Basics", "C03_Logic", "C04_Sets_and_Functions", "C05_Elementary_Number_Theory", "C06_Structures", "C07_Hierarchies", "C08_Groups_and_Rings", "C09_Linear_Algebra", "C10_Topology", "C11_Differential_Calculus", "C12_Integration_and_Measure_Theory", "genindex", "index"], "filenames": ["C01_Introduction.rst", "C02_Basics.rst", "C03_Logic.rst", "C04_Sets_and_Functions.rst", "C05_Elementary_Number_Theory.rst", "C06_Structures.rst", "C07_Hierarchies.rst", "C08_Groups_and_Rings.rst", "C09_Linear_Algebra.rst", "C10_Topology.rst", "C11_Differential_Calculus.rst", "C12_Integration_and_Measure_Theory.rst", "genindex.rst", "index.rst"], "titles": ["<span class=\"section-number\">1. </span>Introduction", "<span class=\"section-number\">2. </span>Basics", "<span class=\"section-number\">3. </span>Logic", "<span class=\"section-number\">4. </span>Sets and Functions", "<span class=\"section-number\">5. </span>Elementary Number Theory", "<span class=\"section-number\">6. </span>Structures", "<span class=\"section-number\">7. </span>Hierarchies", "<span class=\"section-number\">8. </span>Groups and Rings", "<span class=\"section-number\">9. </span>Linear algebra", "<span class=\"section-number\">10. </span>Topology", "<span class=\"section-number\">11. </span>Differential Calculus", "<span class=\"section-number\">12. </span>Integration and Measure Theory", "Index", "Mathematics in Lean"], "terms": {"The": [0, 1, 4, 5, 6, 7, 8, 9, 10, 11, 13], "goal": [0, 1, 2, 3, 4, 5, 8, 9], "thi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "book": [0, 2, 8, 9], "teach": 0, "you": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "formal": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "mathemat": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "us": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "lean": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "4": [0, 1, 2, 4, 5, 7, 8, 9, 10], "interact": [0, 5, 6, 7, 8, 11], "proof": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "assist": [0, 2, 5], "It": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "assum": [0, 1, 2, 3, 4, 6, 7, 8, 9], "know": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "some": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "doe": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "requir": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "much": [0, 2, 4, 6, 7, 8, 9, 10], "although": [0, 3, 4, 5, 6, 7, 8, 9], "we": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "cover": [0, 1, 3, 6, 7, 8, 9, 10], "exampl": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "rang": [0, 2, 3, 4, 7, 8, 9], "from": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "number": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 13], "theori": [0, 1, 2, 3, 6, 7, 8, 9, 10, 13], "measur": [0, 5, 9, 10, 13], "analysi": [0, 5, 8, 10], "focu": [0, 1, 7, 8, 9, 11], "elementari": [0, 3, 5, 7, 8, 9, 13], "aspect": [0, 5, 7], "those": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "field": [0, 1, 5, 6, 7, 8, 10], "hope": [0, 1, 8], "thei": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "ar": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "familiar": [0, 1, 4, 5, 8, 9, 10], "can": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "pick": [0, 6], "them": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "up": [0, 2, 3, 4, 5, 6, 7, 9], "go": [0, 1, 2, 3, 4, 6, 8, 9], "also": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "don": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "t": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "presuppos": 0, "ani": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "background": [0, 7], "method": [0, 2, 3, 4, 5], "seen": [0, 1, 2, 4, 5, 6, 7, 8, 9], "kind": [0, 1, 6, 8, 9], "comput": [0, 2, 3, 4, 5, 7, 8, 10, 11], "program": [0, 1, 2], "write": [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "definit": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "theorem": [0, 2, 4, 5, 7, 8, 9, 10, 11, 13], "regiment": 0, "languag": [0, 1, 2, 3], "like": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "understand": [0, 2, 3, 4, 5, 6, 7, 8, 9], "In": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "return": [0, 2, 3, 4, 5, 7, 8, 9], "provid": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "feedback": 0, "inform": [0, 1, 2, 3, 5, 6, 8, 9], "interpret": [0, 1, 4, 5, 7, 8, 9], "express": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "guarante": [0, 3, 5, 8], "well": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "form": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "ultim": 0, "certifi": 0, "correct": [0, 1, 7], "our": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "learn": [0, 1, 4, 5], "more": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13], "about": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13], "project": [0, 4, 5, 7, 8, 9], "page": [0, 1, 4], "commun": [0, 4], "web": [0, 1, 4], "tutori": 0, "base": [0, 2, 3, 4, 6, 7, 9, 10, 13], "s": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "larg": [0, 6, 9], "ever": [0, 9], "grow": [0, 6, 7], "librari": [0, 1, 2, 3, 4, 5, 7, 9, 10], "mathlib": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "strongli": 0, "recommend": [0, 1, 3], "join": [0, 1, 5], "zulip": [0, 4], "onlin": 0, "chat": 0, "group": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 13], "haven": [0, 2, 6, 9], "alreadi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "ll": [0, 2, 4, 6, 9], "find": [0, 1, 2, 4, 5, 6, 8, 9], "live": [0, 5, 8], "welcom": [0, 1], "enthusiast": 0, "happi": 0, "answer": [0, 5, 9], "question": [0, 4, 6, 9, 11], "offer": [0, 2, 5, 9], "moral": [0, 5, 7], "support": [0, 1, 2, 3, 4, 5, 6, 8, 9], "read": [0, 1, 4, 5, 6, 7, 8, 9], "pdf": 0, "html": 0, "version": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "design": [0, 1, 2, 3, 5, 7, 8, 9], "run": 0, "insid": [0, 1, 2, 3, 7], "vs": [0, 1, 2, 3, 5], "code": [0, 1, 2, 3, 5, 6, 8], "editor": [0, 1], "To": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "instal": [0, 6], "follow": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "instruct": [0, 1, 2, 9], "make": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "sure": [0, 1, 2, 3, 5, 6, 7, 8], "have": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "git": 0, "fetch": 0, "mathematics_in_lean": 0, "repositori": [0, 1], "open": [0, 1, 2, 3, 4, 5, 7, 8, 10, 11], "each": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "section": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "ha": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "an": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "associ": [0, 1, 2, 4, 5, 6, 7, 8, 9, 11], "file": [0, 1, 4, 5, 6, 7, 9], "exercis": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "folder": 0, "mil": 0, "organ": 0, "chapter": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "copi": [0, 3, 4, 6, 7, 8, 9], "experi": [0, 1, 9], "do": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "leav": [0, 1, 2, 3, 5, 6, 7], "origin": [0, 1, 5, 7], "intact": 0, "easier": [0, 1, 3, 4, 6, 9], "updat": 0, "chang": [0, 1, 2, 4, 5, 9, 11], "see": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "below": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "call": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "my_fil": 0, "whatev": [0, 2, 4], "want": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "creat": [0, 1, 4, 6], "your": [0, 1, 2, 3, 5, 6, 7, 9], "own": [0, 1, 4, 5, 6], "At": [0, 1, 2, 4, 5, 6, 8], "point": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "textbook": [0, 1, 2], "side": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "panel": 0, "type": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "ctrl": [0, 1, 2, 4, 5], "shift": [0, 1, 6, 9], "p": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "command": [0, 1, 2, 3, 4, 5, 6, 7, 8], "maco": 0, "doc": 0, "show": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "document": [0, 1, 3, 4, 6], "resourc": 0, "bar": [0, 1, 2, 8], "appear": [0, 1, 2, 5, 6, 7, 8, 9], "press": [0, 8], "select": [0, 9], "soon": [0, 2, 6, 7, 8, 9], "highlight": [0, 2], "menu": [0, 1], "window": [0, 1, 2, 5], "click": [0, 1, 3, 4, 5, 6], "altern": [0, 1, 2, 3, 4, 5, 6, 9], "cloud": 0, "gitpod": 0, "how": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "github": [0, 1], "still": [0, 1, 2, 3, 4, 5, 6, 8, 9, 11], "work": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "describ": [0, 1, 2, 3, 4, 5, 6, 8, 9], "abov": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "progress": [0, 1, 5, 7], "pull": [0, 7, 9], "lake": 0, "ex": [0, 2], "cach": 0, "content": [0, 1, 2, 4, 9], "which": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "why": [0, 2, 4, 6, 7, 8, 9], "suggest": [0, 2, 4, 5, 8, 9], "intend": [0, 1, 2, 5], "while": [0, 1, 2, 6, 7, 8, 9], "contain": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "explan": [0, 7, 8, 9], "hint": [0, 1, 2, 11], "text": [0, 3, 5, 9], "often": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "includ": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10], "one": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "eval": [0, 7, 8], "hello": 0, "world": 0, "should": [0, 1, 2, 3, 4, 5, 6, 7, 9, 10], "abl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 10], "correspond": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "If": [0, 1, 2, 3, 4, 5, 6, 8, 9], "line": [0, 1, 2, 3, 4, 6, 7, 8], "hover": [0, 1, 2, 3, 4, 5], "cursor": [0, 1, 2], "over": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "respons": [0, 1], "pop": 0, "encourag": [0, 1, 2, 3, 4, 5], "edit": 0, "try": [0, 1, 2, 3, 4, 5, 6, 8, 9], "moreov": [0, 1, 4, 5, 9], "lot": [0, 1, 3, 5, 6, 7, 8, 9], "challeng": [0, 1, 2, 3, 5, 10], "rush": 0, "past": [0, 1, 7], "just": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "through": [0, 1, 3, 4, 5, 6, 7, 8, 9], "central": [0, 4], "all": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "when": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "feel": [0, 1, 2, 6, 8, 9], "comfort": 0, "master": [0, 1, 4], "relev": [0, 1, 2, 4, 5, 6, 7, 8, 9], "skill": [0, 1, 2, 3, 4], "free": [0, 1, 7, 8, 9], "move": [0, 1, 2, 6, 8, 9], "alwai": [0, 1, 2, 3, 5, 6, 7, 8], "compar": [0, 5, 6, 8, 9], "solut": [0, 1, 4, 6], "ones": [0, 1, 2, 3, 5, 8, 11], "put": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "simpli": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "tool": [0, 1, 5, 6], "build": [0, 2, 4, 6, 7, 8, 9, 13], "complex": [0, 1, 2, 4, 5, 7, 8, 10, 11], "known": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "depend": [0, 2, 3, 4, 5, 6, 7, 8, 9], "everi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "check": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "print": [0, 3, 4, 5, 11], "\u2115": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "These": [0, 1, 3, 4, 5, 7, 10, 11], "object": [0, 1, 2, 3, 4, 5, 7, 8, 13], "2": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "def": [0, 2, 3, 4, 5, 6, 7, 8, 9], "f": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "x": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "3": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "prop": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "statement": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "fermatlasttheorem": 0, "y": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "z": [0, 1, 2, 5, 6, 7, 8, 9, 10, 11], "n": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "0": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "where": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "itself": [0, 2, 3, 5, 6, 7, 8, 9, 10], "Such": [0, 1, 2, 6], "proposit": [0, 2, 3, 4, 5], "easi": [0, 4, 5, 6, 7, 8, 9], "rfl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "hard": [0, 1, 3, 5, 6, 7], "sorri": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "manag": [0, 1, 4, 5, 9], "construct": [0, 2, 3, 4, 5, 6, 7, 8, 9], "accept": [0, 1, 2, 8, 9], "term": [0, 1, 2, 3, 4, 5, 7, 8, 9], "done": [0, 2, 3, 4, 6, 7, 8, 9], "someth": [0, 1, 2, 4, 6, 8, 9], "veri": [0, 2, 4, 6, 7, 8, 9, 11], "impress": 0, "cheat": [0, 1], "so": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "now": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "game": [0, 6], "left": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "rule": [0, 2, 4, 5, 6, 8, 9], "complementari": 0, "companion": [0, 1], "prove": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "thorough": 0, "underli": [0, 1, 5, 6, 7, 8], "logic": [0, 1, 3, 4, 5, 7, 8, 13], "framework": [0, 8], "core": [0, 4, 5], "syntax": [0, 1, 2, 4, 6, 8], "peopl": [0, 1], "who": [0, 9], "prefer": [0, 1, 2, 3], "user": [0, 6], "manual": [0, 3, 4], "befor": [0, 1, 2, 3, 4, 5, 6, 7, 8], "new": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "dishwash": 0, "person": 0, "hit": [0, 1], "button": 0, "figur": [0, 1, 2, 5], "out": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "activ": 0, "potscrubb": 0, "featur": [0, 2, 4, 7], "later": [0, 1, 2, 4, 5, 6, 7, 8, 9], "sens": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10], "here": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "refer": [0, 1, 2, 4, 5, 6, 8, 9, 10], "back": [0, 1, 2, 5, 6, 7, 8, 9], "necessari": [0, 2, 4, 5, 7, 8], "anoth": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "thing": [0, 1, 2, 3, 4, 5, 6, 8, 9], "distinguish": [0, 5, 6, 7, 9, 10], "place": [0, 1, 2, 5, 8, 9], "greater": [0, 1, 2, 3, 4, 9], "emphasi": [0, 6], "tactic": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "given": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "two": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "wai": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "down": [0, 3, 4, 6, 9], "themselv": [0, 4, 5], "suitabl": [0, 1, 2, 5, 9], "descript": [0, 1, 2, 4, 9], "thereof": 0, "For": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "repres": [0, 1, 2, 3, 4, 5, 6, 10], "fact": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "even": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 11], "m": [0, 1, 2, 4, 6, 7, 8, 9, 10], "nat": [0, 1, 2, 3, 4, 5, 7, 9], "fun": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "k": [0, 2, 4, 5, 7, 8, 9, 10], "hk": [0, 10], "hmn": 0, "rw": [0, 2, 3, 4, 5, 6, 7, 8, 9, 13], "mul_add": [0, 1, 4, 6], "l": [0, 1, 8, 10, 11], "_": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "compress": [0, 1, 9], "singl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 10], "instead": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "style": [0, 1], "same": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "comment": [0, 4], "henc": [0, 2, 3, 4, 5, 6, 8, 9, 10], "ignor": [0, 5, 7, 8, 9], "sai": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "natur": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "rintro": [0, 2, 3, 4, 7, 8, 9], "need": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "twice": [0, 1, 9], "let": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "substitut": [0, 2], "obviou": [0, 4, 5, 6], "ring": [0, 1, 2, 3, 4, 5, 6, 8, 13], "As": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "enter": [0, 1, 2, 3, 7, 9], "displai": [0, 1, 2, 6], "state": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10], "separ": [0, 1, 2, 4, 5, 8], "tell": [0, 2, 3, 4, 5, 6, 7, 8], "what": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "establish": [0, 1, 2, 3, 4, 5], "task": [0, 2, 4, 5, 6, 9], "remain": [0, 1, 2, 3, 5, 6, 9], "replai": 0, "step": [0, 1, 2, 3, 4, 5, 6], "sinc": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "continu": [0, 1, 4, 5, 6, 8, 11], "first": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "introduc": [0, 1, 2, 3, 4, 8, 9, 11], "could": [0, 1, 2, 4, 5, 6, 7, 8, 9], "renam": 0, "decompos": [0, 3], "hypothesi": [0, 1, 2, 3, 4], "assumpt": [0, 1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "second": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "declar": [0, 1, 4, 5, 6, 7, 8], "next": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "rewrit": [0, 1, 2, 3, 4, 5, 6, 8, 9], "replac": [0, 1, 2, 3, 4, 6, 7, 8], "solv": [0, 1, 2, 3, 4, 5, 6, 8, 9], "result": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "abil": 0, "small": [0, 2, 4, 5, 9], "increment": [0, 1], "extrem": [0, 6, 9], "power": [0, 1, 3, 4, 5, 6, 8], "reason": [0, 1, 2, 4, 5, 6, 7, 8, 9], "quicker": 0, "than": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "There": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10, 11], "isn": [0, 2, 3, 4, 6], "sharp": 0, "distinct": [0, 2, 3, 4, 5, 8, 9], "between": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "insert": [0, 2, 4, 5, 7, 8, 9, 10], "did": [0, 2, 6, 9], "phrase": [0, 1, 2, 4, 5, 8], "convers": [0, 2, 4, 7, 8, 9], "short": [0, 1, 2, 3, 4, 5, 8], "middl": [0, 1, 2, 9], "That": [0, 4, 5, 6], "said": [0, 2, 4, 5], "reduc": [0, 2, 3, 4, 5], "liner": 0, "carri": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "But": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "substanti": 0, "autom": [0, 1, 5], "justifi": [0, 1, 2, 9], "longer": [0, 4, 5], "calcul": [0, 2, 4, 5, 13], "bigger": [0, 3, 10], "inferenti": 0, "invok": [0, 1, 9], "simplifi": [0, 2, 3, 4, 5, 9, 11], "specif": [0, 1, 3, 4, 5, 6], "pariti": 0, "automat": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "intro": [0, 1, 2, 3, 4, 5, 6, 7, 9], "simp": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10], "parity_simp": 0, "big": [0, 5, 7, 8, 9, 10], "differ": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "onli": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "its": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "built": [0, 2, 6, 7, 8], "wherea": [0, 1, 2, 3, 5, 7, 9], "top": [0, 6, 7, 8, 9, 10], "meant": [0, 2, 6, 8], "complet": [0, 1, 2, 3, 4, 6, 7, 10], "extens": [0, 1, 6, 9, 10], "rather": [0, 1, 2, 4, 5, 6, 7, 8, 9], "think": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10], "basic": [0, 2, 4, 5, 8, 9, 11, 13], "entri": [0, 5, 7, 8], "brows": [0, 1, 4, 7], "frustrat": [0, 6], "curv": 0, "steep": 0, "newcom": 0, "avail": [0, 1, 2, 4, 5, 6, 7, 8], "round": [0, 1, 5], "clock": 0, "doubt": 0, "enough": [0, 1, 2, 3, 4, 6, 7, 8, 9], "too": [0, 1, 3, 5, 6, 7, 8, 9], "contribut": [0, 3], "develop": [0, 1, 4, 7, 11], "mission": 0, "choos": [0, 2, 3, 4, 5, 6, 7, 9], "dive": 0, "come": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "forewarn": 0, "fundament": [0, 4, 5, 6, 11], "life": [0, 2], "mai": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "never": [0, 6], "acknowledg": 0, "grate": [0, 5], "gabriel": 0, "ebner": 0, "set": [0, 1, 2, 4, 5, 6, 7, 10, 11, 13], "infrastructur": 0, "kim": 0, "morrison": 0, "mario": 0, "carneiro": 0, "help": [0, 1, 2, 3, 4, 5, 6, 8, 9], "port": 0, "takeshi": 0, "ab": [0, 2, 5, 7], "julian": 0, "berman": 0, "alex": 0, "best": 0, "thoma": 0, "brown": 0, "bulwi": 0, "cha": 0, "hanson": 0, "char": 0, "bryan": 0, "gin": 0, "ge": [0, 2, 5], "chen": 0, "steven": 0, "clontz": 0, "mauricio": 0, "collari": 0, "johan": 0, "commelin": 0, "mark": [0, 1, 2, 6, 9], "czubin": 0, "alexandru": 0, "duca": 0, "pierpaolo": 0, "frasa": 0, "deni": 0, "gorbachev": 0, "winston": 0, "de": 0, "greef": 0, "mathieu": 0, "guai": 0, "paquet": 0, "marc": 0, "huisinga": 0, "benjamin": 0, "jone": 0, "k\u00fclshammer": 0, "victor": 0, "liu": 0, "jimmi": 0, "lu": 0, "martin": 0, "c": [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "giovanni": 0, "mascellani": 0, "john": 0, "mcdowel": 0, "bhavik": 0, "mehta": 0, "isaiah": 0, "mindich": 0, "kabelo": 0, "moiloa": 0, "hunter": 0, "monro": 0, "pietro": 0, "monticon": 0, "oliv": 0, "nash": 0, "emanuel": 0, "natal": 0, "filippo": 0, "A": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "e": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "nuccio": 0, "pim": 0, "ott": 0, "bartosz": 0, "piotrowski": 0, "nicola": 0, "rolland": 0, "keith": 0, "yannick": 0, "seurin": 0, "guilherm": 0, "silva": 0, "pedro": 0, "s\u00e1nchez": 0, "terraf": 0, "matthew": 0, "toohei": 0, "alistair": 0, "tucker": 0, "flori": 0, "van": 0, "doorn": 0, "eric": 0, "wieser": 0, "other": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "been": [0, 1, 2, 4, 5, 6, 8, 10], "partial": [0, 1, 2, 3, 5, 6, 7, 8], "hoskinson": 0, "center": [0, 9], "nut": 1, "bolt": 1, "gener": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "without": [1, 2, 4, 5, 6, 7, 8, 9, 10], "net": 1, "hand": [1, 2, 3, 4, 5, 6, 8, 9], "equal": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "right": [1, 2, 3, 4, 5, 6, 8, 9, 10], "tantamount": [1, 3], "name": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "b": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "real": [1, 2, 3, 4, 5, 6, 8, 9, 10, 11], "mul_assoc": [1, 2, 4, 5, 6, 7], "mul_comm": [1, 2, 4, 5, 6, 7], "elimin": 1, "explicitli": [1, 2, 3, 5, 6, 7, 8, 9, 10], "purpos": [1, 2, 3, 4, 5, 6, 8, 9], "illustr": [1, 2, 3, 4, 5, 7], "multipl": [1, 2, 3, 4, 5, 6, 7, 8, 10], "written": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "howev": [1, 2, 5, 6, 7, 8, 9, 10], "good": [1, 2, 3, 4, 5, 6, 7, 8, 9], "mind": [1, 2, 5, 6, 7], "notat": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "convent": [1, 5, 7, 11], "parenthes": [1, 2, 3, 4], "\u211d": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "import": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "begin": [1, 2, 3, 4, 5, 6], "sake": [1, 4], "breviti": [1, 5], "suppress": 1, "happen": [1, 6, 9], "charact": [1, 3, 6], "r": [1, 2, 4, 5, 6, 7, 8, 9], "symbol": [1, 2, 5, 6, 7], "doesn": [1, 2, 7, 8, 9], "until": [1, 4, 6, 9], "space": [1, 2, 3, 5, 6, 7, 11, 13], "tab": [1, 3, 4], "kei": [1, 4, 5, 7, 8, 9], "curiou": [1, 6], "abbrevi": [1, 2, 3, 5, 8], "get": [1, 2, 3, 4, 6, 7, 8, 9, 10, 13], "access": [1, 3, 5, 6, 7, 8, 9, 11], "keyboard": 1, "easili": [1, 4, 5, 6, 7, 8], "backslash": [1, 3], "lead": [1, 2, 4, 5, 6, 7, 8, 9], "lean4": 1, "input": [1, 3, 8, 9], "leader": 1, "report": 1, "current": [1, 2, 5, 6], "infoview": [1, 6], "typic": [1, 7], "might": [1, 2, 3, 4, 5, 7], "look": [1, 2, 3, 4, 6, 7, 8, 9], "1": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "h\u2081": [1, 2, 3, 4], "prime": [1, 2, 3, 5, 6, 7, 8, 13], "h\u2082": [1, 3, 4], "h\u2083": [1, 3], "denot": [1, 3, 4, 6, 7, 8, 9], "context": [1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "plai": [1, 3, 4, 6, 7, 8, 9], "three": [1, 2, 4, 5, 7, 9], "label": [1, 2], "everyth": [1, 2, 6, 9], "identifi": [1, 2, 4, 8], "subscript": [1, 8], "h": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "legal": 1, "would": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "h1": [1, 2, 3, 4, 5], "h2": [1, 2, 3, 5], "h3": 1, "foo": [1, 5], "baz": 1, "last": [1, 2, 3, 4, 5, 6, 7, 9], "sometim": [1, 2, 3, 4, 5, 6, 7, 8, 9], "target": [1, 6, 7, 8, 9, 11], "combin": [1, 2, 5, 6, 7, 8, 9], "practic": [1, 2, 3, 6, 7, 9], "mean": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "usual": [1, 2, 3, 4, 5, 7, 8, 9, 11], "clear": [1, 2, 4, 5, 6], "case": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "With": [1, 3, 4, 6, 9], "arrow": [1, 2, 6, 9], "revers": [1, 2, 3, 5, 9], "note": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "noth": [1, 2, 3, 4, 5, 6, 7], "argument": [1, 2, 3, 4, 5, 6, 7, 8, 9], "tri": [1, 2, 4, 6], "match": [1, 2, 5], "pattern": [1, 2, 3, 5, 6], "local": [1, 2, 6, 9, 10], "d": [1, 2, 4, 5, 7, 8, 10], "sub_self": [1, 2], "hyp": 1, "list": [1, 2, 3, 4, 5, 8], "comma": [1, 8], "squar": [1, 2, 4, 5, 6, 7, 8], "bracket": [1, 2, 5, 6, 7], "after": [1, 2, 4, 6, 8, 9, 10], "trick": [1, 2, 4, 6, 10], "variabl": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "onc": [1, 2, 3, 4, 5, 6, 7, 9, 11], "outsid": [1, 4, 8], "inspect": 1, "reveal": [1, 8], "inde": [1, 5, 6, 7, 8, 9, 10], "delimit": 1, "scope": [1, 2, 3, 5, 7, 8], "end": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "block": [1, 4, 7], "final": [1, 2, 3, 5, 7, 8, 9, 11], "recal": [1, 2, 4, 5, 7, 9, 11], "introduct": [1, 2, 7, 9, 13], "determin": [1, 5, 7, 8, 9], "both": [1, 2, 3, 4, 5, 6, 7, 9, 10], "expect": [1, 2, 3, 4, 5, 6, 7, 8, 9], "rais": [1, 4], "error": [1, 2, 3, 6], "explain": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "output": [1, 7], "meanwhil": [1, 4], "take": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "two_mul": 1, "add_mul": [1, 6], "distribut": [1, 4, 5, 6], "addit": [1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "add_assoc": [1, 4, 5, 6], "precis": [1, 3, 7, 8, 9, 10], "possibl": [1, 2, 3, 4, 5, 7, 9], "calc": [1, 2, 3, 5, 7, 9], "keyword": [1, 2, 4, 5], "notic": [1, 2, 3, 4, 5, 7, 9], "finicki": 1, "underscor": [1, 2, 3, 8], "justif": [1, 2], "format": 1, "indic": [1, 2, 3, 5, 6], "indent": 1, "One": [1, 2, 3, 4, 5, 6, 7, 8, 9], "outlin": [1, 2, 4, 9], "modulo": [1, 4, 5], "individu": 1, "pure": [1, 9], "littl": [1, 2, 9, 10], "underneath": [1, 3], "pow_two": [1, 4], "mul_sub": 1, "add_sub": 1, "sub_sub": 1, "add_zero": [1, 5, 6], "perform": [1, 2, 3], "exact": [1, 2, 3, 4, 5, 7, 8, 9], "becaus": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "exactli": [1, 2, 3, 5, 6, 7, 9], "close": [1, 2, 3, 6, 7, 8, 10, 11], "bit": [1, 2, 4, 6, 7, 8, 9], "commut": [1, 2, 3, 4, 5, 6, 7, 8, 10], "long": [1, 2, 3, 5, 6, 7, 8, 10], "axiom": [1, 2, 3, 5, 6, 7, 8, 9, 11], "indirectli": 1, "data": [1, 2, 4, 5, 6, 8, 9], "similar": [1, 2, 3, 5, 6, 7, 8, 9], "common": [1, 2, 3, 4, 5, 7, 8, 9], "variat": [1, 3, 4, 5, 9, 10], "nth_rw": 1, "allow": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "particular": [1, 2, 5, 6, 7, 8, 9], "instanc": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "enumer": [1, 2], "start": [1, 2, 3, 4, 6, 7, 8, 9, 10, 11, 13], "occurr": 1, "consist": [1, 3, 5, 6, 7, 8, 9, 10], "collect": [1, 2, 3, 5, 8, 9, 11], "oper": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "time": [1, 4, 5, 6, 8, 9, 10, 11], "constant": [1, 2, 7, 11], "mapsto": [1, 5], "abelian": [1, 5, 6, 8], "negat": [1, 5, 13], "invers": [1, 3, 5, 6, 7, 8, 10, 11], "add_comm": [1, 4, 5, 6, 7], "zero_add": [1, 4, 5, 6], "neg_add_cancel": [1, 5], "mul_on": [1, 5, 6, 7], "one_mul": [1, 2, 5, 6], "being": [1, 3, 5, 7, 8, 9, 10], "suffic": [1, 2, 3, 7, 9], "give": [1, 2, 3, 4, 6, 7, 8, 9, 11], "element": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "concret": [1, 2, 4, 5, 6, 8, 9], "integ": [1, 2, 4, 6, 7, 13], "abstract": [1, 2, 5, 6, 7, 8, 9], "character": [1, 3, 4, 8, 9, 10], "axiomat": [1, 2, 3, 5], "train": [1, 6], "recogn": [1, 2, 4, 5, 6, 9], "appropri": [1, 2, 3, 5, 6], "\u2124": [1, 4, 5, 6, 7, 8], "ration": [1, 2, 4, 9], "\u211a": [1, 4, 7, 8, 9], "\u2102": [1, 5, 7, 8, 10], "extend": [1, 3, 4, 5, 6, 9, 11], "order": [1, 2, 3, 4, 5, 6, 8, 9, 10], "Not": [1, 5, 9], "properti": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "hold": [1, 2, 3, 4, 5, 7, 8, 9, 11], "arbitrari": [1, 2, 3, 4, 5, 7, 8], "taken": [1, 2], "cours": [1, 2, 4, 6, 7, 8, 9, 10, 11], "linear": [1, 2, 5, 7, 9, 13], "matric": [1, 5, 7, 13], "fail": [1, 2, 4, 5, 6, 8, 9, 11], "commr": [1, 2, 5, 7], "unchang": [1, 2], "linarith": [1, 2, 4, 5], "permiss": 1, "strike": [1, 2], "balanc": 1, "concis": [1, 5, 7], "readabl": [1, 2, 3, 8, 9], "strengthen": [1, 2, 4], "deriv": [1, 2, 4, 7, 10, 11], "most": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "organiz": 1, "mechan": [1, 2, 5], "namespac": [1, 2, 3, 4, 5, 7, 8, 9], "full": [1, 2, 3, 4, 5, 6, 7, 8, 9], "shorter": [1, 3, 4, 7, 9], "avoid": [1, 2, 3, 4, 5, 6, 7, 10], "due": [1, 6], "clash": 1, "myre": 1, "add_right_neg": 1, "effect": [1, 3, 6, 9], "temporarili": [1, 2], "reprov": [1, 7, 8], "care": [1, 2, 3, 5, 8], "earlier": [1, 7, 8], "pai": [1, 2, 6, 7, 9], "attent": [1, 2, 4, 6, 7, 9], "curli": [1, 2, 8], "implicit": [1, 2, 5, 6, 7, 8, 9, 10], "moment": [1, 2, 5], "worri": [1, 3, 4, 5, 7], "neg_add_cancel_left": 1, "add_neg_cancel_right": 1, "add_left_cancel": 1, "add_right_cancel": 1, "plan": [1, 6, 9], "brace": [1, 8], "imagin": 1, "situat": [1, 3, 6, 7, 9], "draw": [1, 5, 6], "conclus": [1, 2, 4], "hypothes": [1, 2, 3, 4, 5], "redund": [1, 5, 8, 9, 11], "few": [1, 2, 3, 4, 9], "extra": [1, 2, 3, 5, 6, 7, 9], "oner": 1, "complic": [1, 2, 6, 7, 8], "tediou": [1, 2, 6], "suppos": [1, 2, 3, 4, 5, 9], "infer": [1, 2, 3, 5, 6, 7, 8], "mul_zero": [1, 5, 6], "serv": [1, 3, 4, 5, 11], "therefor": [1, 4, 5, 8, 9], "promot": 1, "modular": 1, "subproof": 1, "wa": [1, 3, 7], "except": [1, 2, 5, 7], "ad": [1, 2, 3, 4, 5, 6, 8, 9], "variant": [1, 2, 7, 9], "whose": [1, 2, 4, 5, 6, 7, 8, 9, 10], "necessarili": [1, 8, 11], "miss": [1, 3, 4], "piec": [1, 4, 5, 6, 7, 9], "either": [1, 2, 3, 5, 6, 9], "becom": [1, 4, 5, 6, 9], "technic": [1, 5, 6, 8], "strictli": [1, 2, 10], "less": [1, 2, 3, 4, 5, 6, 7, 8, 9], "script": 1, "slightli": [1, 6, 7, 8, 9, 10], "clearer": [1, 3, 5], "human": 1, "reader": [1, 8, 9], "maintain": 1, "evolv": 1, "rememb": [1, 2, 3, 4, 5, 6, 7, 8, 9], "zero_mul": [1, 4, 5, 6], "By": [1, 3, 5, 6, 7, 8], "neg_eq_of_add_eq_zero": 1, "eq_neg_of_add_eq_zero": 1, "neg_zero": 1, "neg_neg": 1, "had": [1, 6, 8], "annot": [1, 2, 3, 4, 5, 6], "third": [1, 2, 3, 5, 9], "specifi": [1, 2, 3, 4, 5, 8, 9, 10, 11], "imposs": 1, "default": [1, 2, 3, 4, 5, 6, 7, 10], "subtract": [1, 4, 5], "provabl": [1, 3, 6, 9], "sub_eq_add_neg": 1, "On": [1, 2, 3, 5, 6, 8, 9, 11], "defin": [1, 2, 3, 4, 6, 7, 8, 9, 10, 11, 13], "reflex": [1, 2, 5], "present": [1, 2, 4, 7, 9], "forc": [1, 2, 3, 7, 8], "unfold": [1, 2, 3, 4, 5, 9], "deal": [1, 2, 3, 4, 5, 8, 9], "equat": [1, 2, 3, 4, 5], "interchang": 1, "self_sub": 1, "effort": [1, 4], "one_add_one_eq_two": 1, "norm_num": [1, 2, 4, 5, 8], "strength": 1, "weaker": [1, 2], "notion": [1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "addgroup": [1, 5, 7], "otherwis": [1, 2, 3, 4, 5, 7], "addcommgroup": [1, 7, 8], "commgroup": 1, "g": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "inv_mul_cancel": [1, 5], "\u00b9": [1, 3, 5, 6, 7, 8, 9], "cocki": 1, "helper": 1, "along": [1, 4, 7, 9], "mul_inv_cancel": [1, 5, 7], "mul_inv_rev": 1, "non": [1, 3, 6, 7, 8, 9, 11], "abel": [1, 7], "noncomm_r": 1, "seem": [1, 2, 4, 6, 9, 10], "odd": [1, 2, 3, 4, 8], "partli": [1, 6, 7], "histor": [1, 7], "conveni": [1, 2, 3, 5, 6, 7, 8, 9], "great": [1, 5], "sort": [1, 3, 4], "inequ": [1, 2, 6, 9], "le": [1, 5, 6], "whenev": [1, 2, 4, 5, 8], "consid": [1, 2, 3, 4, 5, 6, 7, 9, 10, 11], "le_refl": [1, 2], "le_tran": [1, 2], "detail": [1, 2, 3, 4, 5, 6, 7], "unless": [1, 2, 5], "realli": [1, 2, 3, 4, 6, 7, 8, 9], "insist": [1, 6], "discuss": [1, 2, 4, 5, 6, 7, 8, 9, 10], "implic": [1, 8, 9, 13], "h\u2080": [1, 2, 3, 4, 9], "dot": [1, 7, 8, 9], "option": [1, 2, 4, 5, 6, 9], "within": [1, 2, 9], "visibl": 1, "must": [1, 5, 6, 8, 9], "decreas": [1, 5], "mode": [1, 2, 5], "entir": [1, 3, 5, 9, 10], "lt_of_le_of_lt": [1, 2], "lt_of_lt_of_l": 1, "lt_tran": [1, 2], "togeth": [1, 2, 3, 4, 5, 7, 9], "handl": [1, 3, 4, 6, 7], "arithmet": 1, "5": [1, 2, 5, 7, 8, 9, 10], "pass": [1, 5], "exp_le_exp": 1, "mpr": [1, 2, 5, 9], "exp": [1, 3], "applic": [1, 2, 5, 7, 11], "function": [1, 2, 4, 5, 6, 7, 8, 10, 11, 13], "compound": [1, 2, 9], "pars": [1, 3, 7], "exp_lt_exp": 1, "log_le_log": 1, "log": [1, 3, 11], "log_lt_log": 1, "add_le_add": [1, 2], "add_le_add_left": 1, "add_le_add_right": 1, "add_lt_add_of_le_of_lt": 1, "add_lt_add_of_lt_of_l": 1, "add_lt_add_left": 1, "add_lt_add_right": 1, "add_nonneg": [1, 5], "add_po": 1, "add_pos_of_pos_of_nonneg": 1, "exp_po": [1, 3], "bi": [1, 2, 5], "lr": 1, "iff": [1, 3, 7, 8, 9, 10, 11, 13], "connect": [1, 3, 5, 8, 9], "equival": [1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "mp": [1, 2, 3, 4, 9], "forward": [1, 2, 5, 7, 9], "direct": [1, 2, 3, 6, 7, 9, 10], "stand": [1, 2, 4, 5, 6, 7, 8, 9, 10], "modu": 1, "ponen": 1, "respect": [1, 2, 3, 4, 5, 7, 8, 9], "thu": [1, 3, 4, 5, 9], "again": [1, 2, 3, 4, 5, 6, 7, 8, 9], "numer": [1, 4, 5], "constitut": 1, "part": [1, 2, 3, 4, 5, 6, 8, 9, 11], "strategi": [1, 2, 4], "api": 1, "reli": [1, 2, 5, 9], "guess": [1, 2, 3, 4, 5, 8], "cmd": [1, 2], "mac": [1, 2], "a_of_b_of_c": 1, "approxim": 1, "loud": 1, "probabl": [1, 5, 6, 9], "add_l": 1, "choic": [1, 2, 3, 5, 8, 9], "exist": [1, 2, 3, 6, 7, 8, 9], "jump": [1, 4, 5, 9], "nearbi": [1, 4], "sq_nonneg": 1, "delet": [1, 2, 3], "uncom": 1, "previou": [1, 2, 3, 5, 6, 7, 9, 10, 11], "confirm": [1, 2, 3, 4], "finish": [1, 2, 3, 4, 7], "job": 1, "pow_two_nonneg": [1, 2], "tend": [1, 9], "around": [1, 3, 6, 7, 8, 9, 11], "binari": [1, 2, 4, 5, 6, 8], "increas": 1, "worth": [1, 2, 5], "definition": [1, 4, 5, 6, 9], "principl": [1, 2, 3, 4, 6, 8, 10], "favor": [1, 5], "timesav": 1, "clever": 1, "involv": [1, 2, 4, 5, 6, 7, 8, 9], "nice": [1, 2, 4, 6, 7, 8, 9], "idea": [1, 2, 3, 5, 6, 8, 9], "abs_l": [1, 5], "constructor": [1, 2, 3, 4, 5, 6], "split": [1, 2, 3, 4], "conjunct": [1, 6, 13], "congratul": [1, 2, 4], "min": [1, 2, 9, 11], "uniqu": [1, 2, 3, 4, 5, 7, 8, 9], "min_le_left": 1, "min_le_right": 1, "le_min": 1, "max": [1, 2, 6, 8, 9, 11], "pair": [1, 2, 4, 5, 7, 9], "act": [1, 7, 8], "curri": 1, "logician": 1, "haskel": 1, "bind": [1, 3], "tighter": [1, 3], "infix": [1, 6], "le_antisymm": [1, 2], "usag": 1, "inconsist": [1, 8], "outer": 1, "level": [1, 2, 6, 8], "nest": [1, 2], "bother": [1, 3], "repetit": [1, 6], "foreshadow": 1, "univers": [1, 3, 5, 7, 8, 9, 13], "quantifi": [1, 3, 4, 5, 7, 9, 13], "desir": [1, 3, 6, 7, 9], "implicitli": [1, 2], "repeat": [1, 4, 5, 6], "mani": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11, 13], "shorten": [1, 2, 7], "Of": [1, 2, 4, 6, 7, 8, 9, 10, 11], "interest": [1, 2, 3, 5, 6, 8, 9], "vice": [1, 3], "versa": [1, 3], "word": [1, 2, 3, 4, 5, 7, 8, 9], "switch": [1, 6], "transit": [1, 2, 5, 9], "total": 1, "satisfi": [1, 3, 4, 5, 6, 9, 10], "disjunct": [1, 3, 13], "stick": [1, 2, 9, 10], "aux": [1, 2, 4, 9], "valu": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "yield": [1, 2, 3, 4, 5, 9], "made": [1, 2, 3, 5, 8, 9], "manifest": [1, 9], "triangl": [1, 2, 5], "abs_add": [1, 2], "add_sub_cancel_right": 1, "sub_add_cancel": 1, "relat": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "divis": [1, 2, 4, 5, 6, 8], "Be": [1, 3], "ordinari": [1, 2, 4, 5, 7, 8, 9], "unicod": [1, 3, 6], "obtain": [1, 2, 4, 5, 9, 10], "dvd": 1, "dvd_tran": 1, "dvd_mul_of_dvd_left": 1, "dvd_mul_left": 1, "expon": 1, "expand": [1, 2, 3, 4, 5, 6, 8], "w": [1, 6, 8], "greatest": [1, 5, 9], "divisor": [1, 2, 4, 5, 7], "gcd": [1, 2, 4], "least": [1, 5, 6, 8, 9], "lcm": 1, "analog": [1, 2, 3, 4, 5, 8, 9, 10], "divid": [1, 2, 4, 5, 7], "gcd_zero_right": 1, "gcd_zero_left": 1, "lcm_zero_right": 1, "lcm_zero_left": 1, "dvd_antisymm": 1, "complain": 1, "ambigu": [1, 5], "_root_": [1, 3, 4], "saw": [1, 5, 6, 7, 8, 9], "govern": [1, 5], "class": [1, 4, 5, 6, 7, 8, 9, 10, 11], "antisymmetr": [1, 2], "\u03b1": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "partialord": [1, 2], "adopt": 1, "letter": [1, 5, 10], "\u03b2": [1, 2, 3, 5, 6, 8, 9, 11], "\u03b3": [1, 2, 5, 9], "carrier": [1, 5, 6, 7, 8], "greek": [1, 4], "especi": [1, 2, 5, 6, 7, 8, 9], "strict": [1, 2], "somewhat": [1, 3, 9], "lt_irrefl": [1, 2], "lt_iff_le_and_n": 1, "lattic": [1, 5, 6, 7, 9], "inf_le_left": [1, 9], "inf_le_right": 1, "le_inf": 1, "le_sup_left": 1, "le_sup_right": 1, "sup_l": 1, "lower": [1, 2, 4], "bound": [1, 2, 3, 4, 5, 8, 9, 10, 11], "upper": [1, 2], "glb": 1, "lub": 1, "infimum": [1, 6, 7, 8, 9, 11], "supremum": [1, 4, 6, 7, 8], "inf": [1, 6, 9], "sup": [1, 4, 9], "further": [1, 9], "matter": [1, 2], "meet": [1, 2, 3, 5], "keep": [1, 3, 5, 6, 7], "dictionari": 1, "subset": [1, 2, 3, 5, 9, 10], "domain": [1, 2, 3, 4, 5, 7, 9], "boolean": 1, "truth": [1, 4], "fals": [1, 2, 3, 4, 6], "true": [1, 2, 3, 6, 8, 9], "posit": [1, 3, 4, 5, 9, 11], "subspac": [1, 6, 13], "vector": [1, 3, 6, 7, 10, 13], "intersect": [1, 3, 5, 6, 7, 8, 9, 11], "sum": [1, 2, 4, 5, 6, 7, 9], "inclus": [1, 3, 7, 8, 9], "topolog": [1, 5, 6, 10, 13], "union": [1, 3, 4, 5, 6, 7, 8, 10, 11], "intermedi": [1, 6, 8, 9], "produc": [1, 2, 7, 10], "auto": [1, 6], "mysteri": [1, 5, 6], "unapp": 1, "tran": [1, 2, 4, 5, 6, 7, 8], "issu": [1, 4, 5, 6, 8, 9], "directli": [1, 2, 4, 5, 6, 8, 9], "inf_comm": [1, 7], "inf_assoc": 1, "sup_comm": 1, "sup_assoc": 1, "absorpt": 1, "law": [1, 7], "absorb1": 1, "absorb2": 1, "found": [1, 5, 7, 8, 10], "inf_sup_self": 1, "sup_inf_self": 1, "distriblattic": 1, "inf_sup_left": 1, "inf_sup_right": 1, "sup_inf_left": 1, "sup_inf_right": 1, "shown": [1, 5, 10, 11], "explicit": [1, 2, 5, 6, 8, 9], "nondistribut": 1, "finit": [1, 3, 4, 5, 7, 8, 9, 10, 11], "impli": [1, 2, 3, 4, 5, 8, 9], "larger": [1, 9], "compat": [1, 7, 9], "strictorderedr": 1, "mul_po": [1, 4], "mul_nonneg": 1, "coupl": [1, 2, 6, 8, 9], "bewar": [1, 6, 8], "metric": [1, 5, 10, 13], "equip": [1, 3, 5, 6, 7, 9, 10, 11], "distanc": [1, 2, 9, 10], "dist": [1, 9], "map": [1, 2, 3, 5, 6, 7, 9, 13], "metricspac": [1, 9, 10], "dist_self": 1, "dist_comm": [1, 9], "dist_triangl": [1, 9], "nonneg": [1, 5], "nonneg_of_mul_nonneg_left": 1, "dist_nonneg": [1, 9], "dealt": 2, "simpl": [2, 4, 5, 6, 10], "absolut": 2, "\u03b5": [2, 9, 10], "though": [2, 3, 4, 5], "treat": [2, 3, 5, 6, 7, 9, 10], "appli": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "my_lemma": 2, "\u03b4": [2, 9], "hb": [2, 9], "subsequ": [2, 4, 9], "lemma": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "mention": [2, 3, 5, 6, 7, 9], "my_lemma2": 2, "stage": [2, 5, 6], "my_lemma3": 2, "epo": 2, "ele1": 2, "xlt": 2, "ylt": 2, "essenti": [2, 3, 5, 7, 9], "colon": [2, 8], "off": [2, 3, 4], "my_lemma4": 2, "abs_mul": 2, "mul_le_mul": 2, "abs_nonneg": 2, "mul_lt_mul_right": 2, "extract": [2, 9], "hidden": 2, "expos": [2, 9], "predic": [2, 3, 4, 6, 7, 8, 9, 10], "fnub": 2, "fnlb": 2, "lambda": [2, 5], "hfa": 2, "hgb": 2, "dsimp": [2, 3, 5, 7, 8], "simplif": [2, 3, 4], "contract": 2, "anyhow": 2, "control": 2, "transform": [2, 3], "rest": [2, 3, 5, 7, 9], "routin": 2, "nnf": 2, "nng": 2, "nna": 2, "codomain": [2, 4, 9], "structur": [2, 4, 6, 7, 9, 10, 11, 13], "monoid": [2, 3, 4, 6, 8, 13], "fnub_add": 2, "orderedcanceladdcommmonoid": 2, "high": [2, 7], "monoton": [2, 6, 9], "nondecreas": [2, 4], "placehold": 2, "Or": [2, 3, 8], "backward": [2, 9], "subgoal": 2, "mf": 2, "mg": 2, "aleb": 2, "flag": [2, 3], "squiggli": 2, "marker": 2, "nnc": 2, "bbb": [2, 5], "fneven": 2, "fnodd": 2, "ef": 2, "eg": 2, "og": 2, "rid": 2, "won": [2, 4, 6, 7, 9], "cannot": [2, 3, 4, 5, 6, 7, 8, 9], "contrari": 2, "syntact": 2, "reduct": [2, 3, 5], "erw": 2, "harder": [2, 5, 8], "spot": 2, "manipul": [2, 5, 7, 8, 9], "foundat": [2, 3, 4, 5, 7, 8], "mundan": 2, "assert": [2, 3, 6, 7], "contrast": [2, 3, 5, 6, 9], "zermelo": 2, "fraenkel": 2, "sin": [2, 10], "co": [2, 7], "zf": 2, "defect": [2, 6, 9], "theoret": [2, 3, 8, 9], "motiv": [2, 8], "detect": 2, "meaningless": 2, "independ": [2, 3, 5, 8], "continuum": 2, "meta": [2, 6], "beyond": [2, 6, 10], "ask": [2, 4, 5, 6, 7, 9], "xs": [2, 3], "refl": [2, 3, 5, 6, 7, 8], "setub": 2, "inject": [2, 3, 4, 6, 7, 8, 9], "x_1": [2, 3], "x_2": [2, 3], "x\u2081": [2, 3, 5, 9], "x\u2082": [2, 3, 5], "add": [2, 4, 5, 6, 7, 8, 9, 10], "nonzero": [2, 4, 5, 11], "sourc": [2, 9], "inspir": 2, "add_left_inj": 2, "composit": [2, 3, 5, 6, 7, 8, 9], "injg": 2, "injf": [2, 3], "canon": [2, 3, 4, 5, 8], "exhibit": [2, 9], "anonym": [2, 3, 4, 5, 7], "angl": 2, "certain": [2, 6, 9], "fnhasub": 2, "fnhaslb": 2, "ubf": 2, "ubg": 2, "rcase": [2, 3, 4, 9], "ubfa": 2, "ubgb": 2, "unpack": [2, 3], "main": [2, 6, 8, 9, 10], "els": [2, 3, 4, 8], "turn": [2, 3, 4, 5, 6, 8, 9, 10], "fn_ub_add": 2, "lbf": 2, "lbg": 2, "recurs": [2, 3, 5, 13], "arbitrarili": [2, 9], "assign": [2, 3, 5, 6, 7], "compon": [2, 3, 5, 8, 9, 11], "destruct": 2, "tag": [2, 3, 6], "chosen": [2, 5], "intern": [2, 5, 7], "primit": [2, 3], "scientist": 2, "sight": [2, 6], "hurt": 2, "chanc": 2, "yourself": [2, 5], "compani": 2, "old": [2, 5, 6, 8], "chestnut": 2, "product": [2, 4, 5, 6, 7, 9, 11], "magic": [2, 5, 6], "verifi": 2, "sumofsquar": 2, "sumofsquares_mul": 2, "sosx": 2, "sosi": 2, "xeq": [2, 3], "yeq": 2, "insight": 2, "gaussian": [2, 7, 13], "i": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "sqrt": [2, 3, 4, 5], "norm": [2, 5, 9, 13], "reflect": 2, "di": [2, 5], "xy": [2, 5], "cryptic": 2, "easiest": [2, 4], "perspicu": 2, "6": [2, 4, 5, 6, 7, 8, 9, 10], "divab": 2, "divbc": 2, "beq": 2, "ceq": 2, "And": [2, 4, 6, 9], "pretti": [2, 6, 7, 8, 9], "Then": [2, 3, 5, 6, 7, 8, 9, 11], "divac": 2, "alpha": [2, 3], "beta": [2, 3], "surject": [2, 3, 7, 8, 9], "mul_div_cancel\u2080": 2, "field_simp": [2, 5], "denomin": [2, 4, 5], "hx": [2, 3, 5, 6, 7, 8, 10], "surjg": 2, "surjf": [2, 3], "contradict": [2, 3, 4], "speak": [2, 5, 7, 9], "irreflex": 2, "asymmetri": 2, "lt_asymm": 2, "eventu": [2, 3, 9], "fnuba": 2, "not_le_of_gt": 2, "not_lt_of_g": [2, 4, 5], "lt_of_not_g": 2, "le_of_not_gt": 2, "snippet": [2, 4, 5, 7, 8], "counterexampl": [2, 10], "monof": 2, "four": [2, 5], "valid": 2, "far": [2, 3, 6, 8, 9], "q": [2, 4, 5, 6, 7, 8, 9], "fourth": 2, "straightforward": [2, 6], "difficult": [2, 6], "conclud": [2, 10], "nonexist": 2, "contradictori": 2, "classic": [2, 3, 4, 7, 8], "by_contra": [2, 4], "not_not": 2, "front": 2, "push": [2, 4, 7, 9], "inward": 2, "facilit": [2, 8, 9], "push_neg": [2, 3, 4], "restat": [2, 6, 7, 8], "contrapos": [2, 3, 4], "similarli": [2, 3, 4, 5, 7, 8], "yet": [2, 3, 4, 5, 6, 8, 9], "semicolon": [2, 4], "falso": 2, "anyth": [2, 5, 9], "elim": 2, "strang": [2, 4, 7, 8], "fairli": 2, "reach": [2, 6], "37": 2, "exfalso": 2, "absurd": [2, 4], "slick": 2, "drop": 2, "manner": [2, 5], "techniqu": [2, 9], "variou": [2, 3, 5, 6, 8, 11], "xltz": 2, "zlty": 2, "10": [2, 8, 9], "7": [2, 4, 5, 7, 8], "behav": [2, 3, 6, 8, 9], "roughli": [2, 3, 4], "friend": [2, 5], "were": [2, 4, 5, 8, 9], "inscrut": [2, 3], "gadget": [2, 9], "auxiliari": [2, 9], "pow_eq_zero": [2, 4], "doubl": [2, 3], "symmetr": [2, 3, 7], "abs_lt": 2, "dvd_gcd_iff": 2, "8": [2, 4, 7, 8, 9], "15": 2, "not_monotone_iff": 2, "aris": 2, "preorder": [2, 6, 9], "pre": [2, 8], "lt_iff_le_not_l": 2, "repeatedli": [2, 9], "instanti": [2, 5, 6, 9], "inl": [2, 3, 8], "inr": [2, 3, 8], "branch": [2, 3, 6], "le_or_gt": 2, "abs_of_nonneg": [2, 5], "abs_of_neg": 2, "against": 2, "immedi": [2, 3, 5, 6, 8], "attract": 2, "closer": [2, 9], "advantag": [2, 3, 4, 5, 7, 10], "myab": 2, "le_abs_self": 2, "neg_le_abs_self": 2, "enjoi": [2, 3, 4, 9], "pun": 2, "lt_ab": 2, "genuin": 2, "vertic": [2, 5, 8], "lt_trichotomi": 2, "xgt": 2, "dvd_mul_right": [2, 4], "eq_zero_or_eq_zero_of_mul_eq_zero": 2, "zero": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "nontrivi": [2, 3, 4, 5, 8, 9, 10], "integr": [2, 10, 13], "isdomain": [2, 7], "whether": [2, 3, 4, 6, 9], "em": [2, 3], "exclud": [2, 4], "by_cas": [2, 3, 4], "dispos": 2, "s_0": [2, 3], "s_1": 2, "s_2": 2, "ldot": [2, 3, 4], "varepsilon": [2, 9], "s_n": [2, 3], "render": [2, 4], "convergesto": 2, "ext": [2, 3, 4, 5, 6, 7, 8], "enabl": [2, 3, 4, 5], "actual": [2, 3, 4, 6, 7, 8, 9], "u": [2, 3, 5, 7, 8, 9, 11], "v": [2, 3, 5, 8, 9], "congr": 2, "reconcil": 2, "peel": 2, "convert": [2, 4, 7, 8], "quit": [2, 6, 9], "zero_lt_on": [2, 4], "fill": [2, 3, 4, 5], "convergesto_const": 2, "\u03b5po": [2, 9], "nge": 2, "abs_zero": 2, "save": 2, "troubl": [2, 3, 5], "pen": [2, 7], "paper": [2, 3, 5, 7, 8, 9, 11], "ns": 2, "nt": 2, "maximum": [2, 4, 9], "implement": [2, 5, 6, 7, 8, 10], "convergesto_add": 2, "cs": 2, "ct": 2, "clean": [2, 9], "\u03b52po": 2, "hs": [2, 4, 7, 9, 11], "ht": 2, "le_of_max_le_left": 2, "le_of_max_le_right": 2, "tricki": [2, 3, 4, 6, 7], "convergesto_mul_const": 2, "acpo": 2, "abs_po": 2, "exists_abs_le_of_convergesto": 2, "strong": [2, 4], "n\u2080": 2, "bpo": [2, 9], "pos\u2080": 2, "div_po": 2, "n\u2081": 2, "convergesto_mul": 2, "sketch": [2, 3, 4, 9], "limit": [2, 6, 9], "bold": 2, "scratch": 2, "convergesto_uniqu": 2, "sa": 2, "sb": 2, "abn": 2, "na": 2, "hna": 2, "nb": 2, "hnb": 2, "absa": 2, "absb": 2, "observ": [2, 4, 9], "everywher": [2, 3, 6, 8, 9, 11], "linearord": 2, "vastli": 2, "awai": [2, 5], "vocabulari": [3, 8], "uniform": [3, 9, 10], "conceptu": [3, 7], "overload": 3, "verbos": 3, "system": [3, 4, 5, 6, 8], "wrong": 3, "ss": 3, "sub": [3, 9, 11, 13], "cap": 3, "un": 3, "cup": 3, "univ": [3, 9, 10, 11], "empti": [3, 4, 5, 7, 9, 11], "member": [3, 9], "membership": [3, 4, 6, 7, 8], "mem": [3, 8], "notin": 3, "ident": [3, 4, 5, 6, 7, 8, 9, 13], "databas": [3, 4, 6, 9], "unlik": [3, 4], "existenti": [3, 7, 13], "subset_def": 3, "inter_def": 3, "mem_setof": 3, "xu": 3, "mem_inter_iff": 3, "xsu": 3, "phenomenon": 3, "union_def": 3, "mem_union": [3, 4], "xtu": 3, "xt": 3, "unnecessari": [3, 7], "correctli": 3, "special": [3, 4, 5, 6, 7, 8, 9, 11], "rewritten": 3, "diff_eq": 3, "mem_diff": 3, "xstu": 3, "xnt": 3, "xnu": 3, "extension": [3, 5], "unsurprisingli": 3, "harm": 3, "and_comm": 3, "antisymm": 3, "hood": [3, 5, 8], "builder": 3, "not_even_iff_odd": 3, "not_even_iff": 3, "trivial": [3, 4, 7, 8, 9], "eq_two_or_odd": 3, "odd_iff": 3, "confus": [3, 4, 6, 7, 9], "fortun": 3, "agre": 3, "prime_iff": 3, "symm": [3, 4, 5, 6, 7, 8, 9, 10], "rwa": [3, 4, 5], "restrict": [3, 4, 7, 9], "signific": 3, "ball": [3, 10], "bex": 3, "bex_def": 3, "prime_x": 3, "slight": 3, "ssubt": 3, "index": [3, 6, 7, 8, 9], "model": [3, 8, 9], "sequenc": [3, 6, 9, 10, 13], "a_0": 3, "a_1": 3, "a_2": 3, "mem_iunion": 3, "xai": 3, "mem_iint": 3, "mem_iunion\u2082": 3, "mem_iinter\u2082": 3, "exists_prime_and_dvd": 3, "eq_univ": 3, "eq_univ_of_foral": 3, "exists_infinite_prim": 3, "\u2080": [3, 8], "sunion": 3, "sinter": 3, "relationship": [3, 4], "sunion_eq_biunion": 3, "sinter_eq_biint": 3, "preimag": [3, 7, 8, 9], "imag": [3, 4, 6, 7, 8, 9], "tripl": 3, "mem_image_of_mem": 3, "galoi": [3, 5, 8, 9], "image_subset_iff": 3, "represent": [3, 4, 5, 8], "asid": 3, "raini": 3, "dai": 3, "behavior": [3, 6, 9], "nonempti": [3, 7, 9], "condit": [3, 4, 6, 7, 8, 9, 10], "injon": [3, 11], "theme": 3, "rel": [3, 5, 8], "relativ": 3, "xpo": 3, "ypo": 3, "exp_log": 3, "ingredi": [3, 5, 9, 10], "inhabit": [3, 5, 9], "appeal": [3, 6], "choose_spec": 3, "noncomput": [3, 5, 7, 8], "inverse_spec": 3, "dif_po": 3, "dif_neg": 3, "if_po": 3, "if_neg": 3, "fulli": [3, 7, 8, 9], "alon": 3, "leftinvers": 3, "rightinvers": 3, "hack": 3, "half": [3, 7], "dozen": 3, "condens": 3, "cantor": 3, "famou": [3, 7], "j": [3, 7, 8], "intuit": [3, 9], "cardin": [3, 7, 8], "biject": [3, 5, 7, 8], "nineteenth": 3, "centuri": 3, "infinit": [3, 8, 9, 13], "dedekind": 3, "quickli": [3, 7, 11], "behind": [3, 7], "problem": [3, 4, 5, 6, 9], "shade": 3, "region": 3, "diagram": 3, "circ": [3, 5], "scale": 3, "inner": 3, "smaller": [3, 4, 9], "concentr": 3, "unshad": 3, "compos": [3, 5, 7, 9], "disjoint": [3, 7, 11], "sound": [3, 5, 6], "plausibl": 3, "delic": 3, "improv": [3, 4], "confid": 3, "better": [3, 4, 5, 6, 9], "invfun": [3, 5, 8], "leftinverse_invfun": 3, "invfun_eq": 3, "sbaux": 3, "sbset": 3, "s_": 3, "bigcup_": 3, "mathbb": [3, 4, 5, 7], "sbfun": 3, "complement": [3, 8, 9, 11], "outermost": 3, "setminu": 3, "sb_right_inv": 3, "goe": [3, 4, 5, 6, 9], "neither": [3, 5, 6, 8], "nor": [3, 5, 8], "sb_inject": 3, "hf": [3, 7, 9, 10, 11], "a_def": 3, "h_def": 3, "hxeq": 3, "xa": 3, "wlog": 3, "x\u2081a": 3, "resolve_left": 3, "x\u2082a": 3, "not_imp_self": 3, "x\u2082na": 3, "x\u2082eq": 3, "hn": [3, 4, 9, 10], "sb_fun": 3, "bring": [3, 4, 9], "tradeoff": 3, "encapsul": [3, 5, 10], "symmetri": [3, 6], "dwell": 3, "sb_surject": 3, "hg": [3, 9, 10, 11], "gya": 3, "xmem": 3, "sweet": 3, "schroeder_bernstein": 3, "substant": 4, "ancient": 4, "fraction": 4, "lowest": 4, "2c": 4, "4c": 4, "factor": [4, 5, 7, 8], "coprim": [4, 7], "smart": 4, "12": [4, 8], "encount": [4, 6], "algebra": [4, 6, 9, 10, 11, 13], "prime_def_lt": 4, "eq_one_or_self_of_dvd": 4, "prime_p": 4, "17": 4, "commonli": [4, 5], "prime_two": 4, "prime_thre": 4, "broader": [4, 10], "irreduc": [4, 5], "coincid": [4, 5, 9], "rise": [4, 6, 7], "dvd_mul": 4, "even_of_even_sqr": 4, "dvd_of_dvd_pow": 4, "proce": [4, 6], "profici": 4, "prefix": [4, 6, 7], "search": [4, 5, 6], "engin": 4, "hesit": 4, "mul_right_inj": 4, "heart": [4, 7], "irration": 4, "dvd_gcd": 4, "coprime_mn": 4, "sqr_eq": 4, "meq": 4, "dvd_iff_exists_eq_mul_left": 4, "two_l": 4, "le_of_dvd": 4, "approach": [4, 5, 6, 9], "quick": [4, 7, 8, 10], "ne": [4, 5], "occur": 4, "suffici": [4, 9], "primefactorslist": 4, "permut": [4, 7], "prime_of_mem_primefactorslist": 4, "prod_primefactorslist": 4, "primefactorslist_uniqu": 4, "talk": [4, 7, 8, 9, 10], "factorization_mul": 4, "mnez": 4, "nnez": 4, "factorization_pow": 4, "black": [4, 6], "box": 4, "simpa": [4, 7, 10], "nnz": 4, "nsqr_nez": 4, "eq1": 4, "eq2": 4, "add_mul_mod_self_left": 4, "mul_mod_right": 4, "count_factors_mul_of_po": 4, "succ_ne_zero": 4, "succ": [4, 6], "successor": [4, 8], "npow_nz": 4, "dvd_sub": 4, "anywai": [4, 7], "pow_eq": 4, "npowz": 4, "add_sub_cancel": 4, "understood": [4, 9], "quotient": [4, 5, 6, 9, 13], "pictur": [4, 5, 7], "mediat": 4, "headach": 4, "contend": 4, "th": [4, 8], "topic": [4, 5, 6, 7, 8], "enat": 4, "infin": [4, 9, 11], "appreci": 4, "role": [4, 5, 8, 9], "datatyp": 4, "freeli": 4, "translat": [4, 6, 7, 9], "mathematician": [4, 9], "inj": 4, "factori": 4, "fac": 4, "ih": 4, "fac_po": 4, "succ_po": 4, "dvd_fac": 4, "ipo": 4, "il": 4, "of_le_succ": 4, "dvd_mul_of_dvd_right": 4, "crude": 4, "remaind": [4, 5, 7], "pow_succ": 4, "pow_two_le_fac": 4, "finset": [4, 5, 7, 8, 9], "bigoper": [4, 5, 7], "prod": [4, 7, 8, 9, 11], "sum_range_zero": 4, "sum_range_succ": 4, "summat": 4, "prod_range_zero": 4, "prod_range_succ": 4, "deserv": 4, "danger": [4, 5], "ordinarili": [4, 5], "loop": 4, "indefinit": 4, "fix": [4, 6, 7, 8, 9], "mul_left_comm": 4, "placement": 4, "re": [4, 5], "handi": 4, "sum_id": 4, "div_eq_of_eq_mul_right": 4, "sum_sqr": 4, "mynat": 4, "thumb": 4, "decid": [4, 7, 8, 9], "preced": [4, 7], "truncat": 4, "exponenti": 4, "cut": 4, "predecessor": 4, "pred": 4, "mul": [4, 5, 6, 9], "succ_add": 4, "succ_mul": 4, "explor": [4, 8, 9], "standard": [4, 5, 6, 9], "formul": [4, 7, 9], "quirki": 4, "among": 4, "annoi": [4, 6], "h0": 4, "succ_le_succ": 4, "zero_l": [4, 5], "interval_cas": 4, "interv": [4, 9, 11], "decis": [4, 7], "procedur": [4, 6], "revert": 4, "minfac": 4, "smallest": [4, 6, 8, 9], "strong_induction_on": 4, "subsum": 4, "exists_prime_factor": 4, "np": 4, "mltn": 4, "mdvdn": 4, "mne1": 4, "mz": 4, "zero_dvd_iff": 4, "mgt2": 4, "pp": 4, "pdvd": 4, "factorial_po": 4, "dvd_factori": 4, "primes_infinit": 4, "refin": [4, 10], "ple": 4, "p_1": 4, "p_n": 4, "prod_": 4, "p_i": [4, 9], "computation": [4, 8], "test": 4, "decidableeq": [4, 8], "abandon": 4, "ourselv": [4, 6], "subset_iff": 4, "mem_int": 4, "mem_sdiff": 4, "tauto": 4, "dispens": 4, "tautolog": 4, "dvd_prod_of_mem": 4, "eq_of_dvd_of_prim": 4, "prime_q": 4, "preserv": [4, 6, 8, 9], "induction_on": 4, "singleton": 4, "prod_empti": 4, "prod_insert": 4, "mem_of_dvd_prod_prim": 4, "mem_insert": 4, "wrote": 4, "filter": [4, 10, 11, 13], "mem_filt": 4, "aim": [4, 7], "prod_po": 4, "_def": 4, "mem_": 4, "id": [4, 6, 8, 9, 10], "bounded_of_ex_finset": 4, "qk": 4, "lt_succ_of_l": 4, "le_sup": 4, "ex_finset_of_bound": 4, "decidablepr": 4, "lt_succ_iff": 4, "congruent": 4, "p_k": 4, "loss": 4, "27": 4, "mod_4_eq_3_or_mod_4_eq_3": 4, "mul_mod": 4, "mod_lt": 4, "mul_mod_mod": 4, "two_le_of_mod_4_eq_3": 4, "neq": 4, "div_dvd_of_dvd": 4, "div_lt_self": 4, "exists_prime_factor_mod_4_eq_3": 4, "mge2": 4, "mul_div_cancel": 4, "home": [4, 5], "stretch": [4, 5], "remov": [4, 9], "eras": 4, "mem_eras": 4, "readi": [4, 6, 7, 8, 9, 10], "dvd_add_iff_left": 4, "primes_mod_4_eq_3_infinit": 4, "p4": 4, "pltn": 4, "p4eq": 4, "ps": 4, "pne3": 4, "seriou": [4, 6, 9], "feat": 4, "modern": [5, 7], "subject": 5, "consult": 5, "ann": 5, "baanen": 5, "abus": 5, "paramet": [5, 6], "broadest": 5, "constraint": [5, 9], "bundl": [5, 6, 7, 8, 9, 10], "tupl": 5, "hy": [5, 6, 7, 8], "hz": [5, 6], "mypoint1": 5, "mypoint2": 5, "mypoint3": 5, "mk": [5, 6, 7, 8, 9], "former": 5, "latter": [5, 7, 9], "quot": [5, 8, 9], "protect": 5, "add_x": 5, "addalt": 5, "eta": 5, "messier": 5, "view": [5, 6, 7, 9], "y\u2081": 5, "z\u2081": 5, "y\u2082": 5, "z\u2082": 5, "addalt_x": 5, "addalt_comm": 5, "apart": [5, 6], "effici": [5, 7, 8, 9], "scalar": [5, 6, 7, 8, 10], "smul": [5, 6, 7, 8], "smul_distrib": 5, "road": 5, "link": [5, 6], "belong": [5, 6, 9], "simplex": 5, "convinc": 5, "equilater": 5, "interior": [5, 10], "standardtwosimplex": 5, "x_nonneg": 5, "y_nonneg": 5, "z_nonneg": 5, "sum_eq": 5, "swap": 5, "swapxi": 5, "interestingli": [5, 7, 10], "midpoint": 5, "div_nonneg": 5, "weight": 5, "averag": 5, "weightedaverag": 5, "lambda_nonneg": 5, "lambda_l": 5, "fin": [5, 7, 8, 11], "standardsimplex": 5, "sum_eq_on": 5, "div_eq_mul_inv": 5, "sum_mul": 5, "sum_add_distrib": 5, "mul_sum": 5, "islinear": 5, "is_addit": 5, "preserves_mul": 5, "linf": 5, "subtyp": [5, 6, 7, 8, 9], "preal": 5, "val": 5, "sigma": [5, 11], "wherebi": [5, 9], "stdsimplex": 5, "\u03c3": [5, 7], "fst": [5, 8, 9], "snd": [5, 8, 9], "custom": 5, "robust": [5, 6], "interfac": 5, "redefin": [5, 6], "accessor": 5, "weav": 5, "rich": [5, 6], "interconnect": 5, "hierarchi": [5, 7, 8, 13], "clarifi": 5, "cdot": 5, "mathcal": [5, 10], "proxi": 5, "bipartit": 5, "graph": [5, 8], "categori": [5, 8, 9, 10], "morphism": [5, 8, 10, 13], "basi": [5, 8, 9], "discret": 5, "inherit": [5, 6, 7, 8], "polynomi": [5, 8], "coeffici": [5, 7, 8], "dual": [5, 9], "accommod": [5, 7], "almost": [5, 6, 7, 8, 9, 11], "marriag": 5, "heaven": 5, "group\u2081": [5, 6], "inv": [5, 6], "struc": 5, "counterpart": 5, "assur": 5, "groupcat": 5, "group\u2081cat": 5, "str": 5, "capit": 5, "roman": 5, "equiv": [5, 7, 8], "tofun": [5, 6, 8], "right_inv": [5, 8], "left_inv": [5, 8], "creativ": 5, "evid": 5, "coercion": [5, 6, 7, 8, 9, 10], "omit": 5, "perm": [5, 7], "under": [5, 6, 7, 8, 9], "orient": 5, "permgroup": 5, "trans_assoc": 5, "trans_refl": 5, "refl_tran": 5, "self_trans_symm": [5, 7, 8], "grouptheori": 5, "g_1": 5, "g_2": 5, "g_3": 5, "tightli": 5, "isomorph": [5, 7, 8, 10], "Its": [5, 6], "neg": [5, 6, 9, 11], "reproduc": 5, "accompani": 5, "addgroup\u2081": 5, "scheme": 5, "addgrouppoint": 5, "arrang": 5, "mul_inv_cancel_right": 5, "achiev": [5, 6, 9], "silent": [5, 6], "regist": [5, 6, 7, 8], "grp": 5, "contextu": 5, "cue": 5, "synthes": [5, 6], "whole": [5, 8], "_inst_1": 5, "candid": 5, "group\u2082": 5, "mysquar": 5, "my_squar": 5, "remark": [5, 6], "headi": 5, "store": 5, "hasmulgroup\u2082": 5, "hasonegroup\u2082": 5, "hasinvgroup\u2082": 5, "suppli": 5, "accord": [5, 8], "capabl": 5, "chain": 5, "recent": 5, "prioriti": 5, "bad": [5, 6, 8, 9], "artifici": [5, 8], "addgroup\u2082": 5, "subtl": [5, 7, 8, 9], "configur": 5, "invis": [5, 6], "wise": [5, 8], "euclidean": 5, "terminolog": [5, 8], "mid": 5, "imaginari": 5, "gaussint": 5, "im": 5, "pointwis": [5, 9, 10], "root": [5, 6, 7, 8, 13], "ac": 5, "bci": 5, "adi": 5, "bd": 5, "bc": 5, "zero_def": 5, "one_def": 5, "add_def": 5, "neg_def": 5, "mul_def": 5, "zero_r": 5, "zero_im": 5, "one_r": 5, "one_im": 5, "add_r": 5, "add_im": 5, "neg_r": 5, "neg_im": 5, "mul_r": 5, "mul_im": 5, "surprisingli": [5, 6], "concept": [5, 7, 8, 9, 10], "light": 5, "bulb": 5, "skeleton": [5, 8, 9], "scari": 5, "nsmul": [5, 6], "zsmul": [5, 6], "instcommr": 5, "nsmulrec": 5, "zsmulrec": 5, "left_distrib": [5, 6], "right_distrib": [5, 6], "ext_iff": 5, "bq": 5, "archetyp": [5, 8], "eq": 5, "int": [5, 6, 7], "ediv_add_emod": 5, "emod_nonneg": 5, "emod_lt": 5, "unit": [5, 6, 9], "algorithm": 5, "conjug": [5, 7], "frac": 5, "nearest": 5, "vi": 5, "multipli": [5, 8], "emb": 5, "forth": 5, "quadrat": 5, "gaussianint": 5, "stai": 5, "face": [5, 6, 9], "machineri": [5, 6, 8, 9], "adapt": 5, "invest": 5, "pragmat": 5, "seek": 5, "heather": 5, "macbeth": 5, "eleg": 5, "div": 5, "mod": 5, "_add_mod": 5, "abs_mod": 5, "_le": 5, "emod_lt_of_po": 5, "zero_lt_two": 5, "_eq": 5, "sq_add_sq_eq_zero": 5, "linearorderedr": 5, "norm_nonneg": [5, 10], "norm_eq_zero": [5, 10], "norm_po": 5, "norm_mul": [5, 10], "conj": 5, "conj_r": 5, "conj_im": 5, "norm_conj": 5, "bespok": 5, "quad": 5, "record": [5, 6, 8], "div_def": 5, "mod_def": 5, "messi": 5, "nicer": [5, 7, 9], "norm_mod_lt": 5, "norm_y_po": 5, "sq_ab": 5, "gcongr": 5, "ediv_mul_l": 5, "le_of_mul_le_mul_right": 5, "ediv_lt_of_lt_mul": 5, "natab": 5, "coe_natabs_norm": 5, "natabs_of_nonneg": 5, "natabs_norm_mod_lt": 5, "ofnat_lt": 5, "natcast_natab": 5, "not_norm_mul_left_lt_norm": 5, "natabs_mul": 5, "le_mul_of_one_le_right": 5, "ofnat_l": 5, "add_one_le_of_lt": 5, "euclideandomain": 5, "quotient_mul_add_remainder_eq": 5, "quotient_zero": 5, "r_wellfound": 5, "remainder_lt": 5, "mul_left_not_lt": 5, "payoff": 5, "irreducible_iff_prim": 5, "studi": [6, 9], "prematur": 6, "technolog": 6, "simpler": [6, 8], "ring\u2081": 6, "gradual": [6, 9], "bottom": [6, 7, 8, 9], "endow": [6, 7, 8], "one\u2081": 6, "heavier": 6, "inferr": 6, "resolut": 6, "attribut": 6, "ensur": [6, 7, 8, 9], "self": 6, "one\u2082": 6, "usabl": 6, "silli": 6, "affect": 6, "importantli": [6, 7, 8], "habit": [6, 8], "ascript": [6, 7, 8], "messag": 6, "typeclass": [6, 8], "stuck": 6, "metavari": 6, "263": 6, "sever": [6, 8, 9, 11], "unknown": 6, "collis": 6, "builtin": 6, "\ud835\udfd9": 6, "inherit_doc": 6, "diamond": 6, "dia\u2081": 6, "dia": 6, "infixl": 6, "70": 6, "semigroup": 6, "dia_assoc": 6, "semigroup\u2081": 6, "todia\u2081": 6, "previous": 6, "semigroup\u2082": 6, "hurdl": 6, "neutral": [6, 7], "diaoneclass\u2081": 6, "one_dia": 6, "dia_on": 6, "trace": [6, 8], "ters": 6, "attempt": 6, "succe": 6, "success": 6, "set_opt": 6, "synthinst": 6, "monoid\u2081": 6, "hide": [6, 7, 9], "subtleti": [6, 7, 8], "fear": 6, "unrel": 6, "tosemigroup\u2081": 6, "todiaoneclass\u2081": 6, "monoid\u2082": 6, "toone\u2081": 6, "overlap": [6, 7], "tear": 6, "signatur": 6, "restor": 6, "optim": [6, 8, 11], "reusabl": 6, "inv\u2081": 6, "postfix": 6, "inv_dia": 6, "weak": 6, "preliminari": 6, "left_inv_eq_right_inv\u2081": 6, "hba": 6, "hac": 6, "export": 6, "inv_eq_of_dia": 6, "dia_inv": 6, "naiv": [6, 9], "duplic": 6, "to_addit": 6, "semi": [6, 7, 8], "left_inv_eq_right_inv": 6, "left_neg_eq_right_neg": 6, "whatsnew": 6, "addsemigroup\u2083": 6, "add_assoc\u2083": 6, "semigroup\u2083": 6, "mul_assoc\u2083": 6, "addmonoid\u2083": 6, "addzeroclass": 6, "monoid\u2083": 6, "muloneclass": 6, "tomuloneclass": 6, "addcommsemigroup\u2083": 6, "commsemigroup\u2083": 6, "addcommmonoid\u2083": 6, "commmonoid\u2083": 6, "addgroup\u2083": 6, "neg_add": 6, "group\u2083": 6, "inv_mul": 6, "inv_eq_of_mul": 6, "propag": 6, "attr": 6, "mul_inv": [6, 7], "mul_left_cancel\u2083": 6, "mul_right_cancel\u2083": 6, "addcommgroup\u2083": 6, "commgroup\u2083": 6, "demonstr": [6, 9], "semir": [6, 7], "opposit": [6, 9], "gain": 6, "besid": 6, "parent": 6, "ring\u2083": 6, "mulzeroclass": 6, "toaddgroup\u2083": 6, "mayb": 6, "claus": 6, "le\u2081": 6, "50": 6, "\u2081": 6, "preorder\u2081": 6, "partialorder\u2081": 6, "orderedcommmonoid\u2081": 6, "modul": [6, 7, 8], "pretend": [6, 8], "smul\u2083": 6, "infixr": 6, "73": 6, "module\u2081": 6, "zero_smul": 6, "one_smul": [6, 7], "mul_smul": [6, 7], "add_smul": [6, 7, 8], "smul_add": [6, 8], "surpris": 6, "toaddcommgroup\u2083": 6, "inst": 6, "module\u2083": 6, "hunt": [6, 8], "unspecifi": [6, 8], "embark": 6, "quest": 6, "huge": 6, "trap": 6, "refus": [6, 9], "tosmul\u2083": 6, "inst_1": 6, "safe": [6, 7], "selfmodul": 6, "invert": [6, 7, 8], "nsmul\u2081": 6, "zsmul\u2081": 6, "ofnat": 6, "negsucc": 6, "abgrpmodul": 6, "failur": 6, "synth": 6, "indirect": 6, "path": 6, "thank": 6, "offend": 6, "poor": 6, "forget": 6, "http": 6, "inria": 6, "hal": 6, "scienc": 6, "02463336v2": 6, "modifi": 6, "addmonoid\u2084": 6, "nsmul_zero": 6, "nsmul_succ": 6, "mysmul": 6, "stori": [6, 8], "incorpor": 6, "lt\u2081": 6, "comparison": 6, "ismonoidhom\u2081": 6, "unpleas": [6, 9], "chose": 6, "ismonoidhom\u2082": 6, "map_on": [6, 7], "map_mul": [6, 7, 8], "tempt": 6, "higher": 6, "unif": 6, "psycholog": 6, "rare": 6, "adject": 6, "bare": [6, 8], "noun": 6, "argu": 6, "continuous_id": [6, 9], "primari": 6, "monoidhom\u2081": 6, "coefun": 6, "coerc": [6, 7, 8], "coe": 6, "addmonoidhom\u2081": 6, "addmonoid": [6, 7], "map_zero": [6, 7], "map_add": [6, 7, 8, 10], "ringhom\u2081": 6, "minor": [6, 10], "tomonoidhom\u2081": 6, "juggl": 6, "monoidhomclass\u2081": 6, "badinst": 6, "wouldn": 6, "priori": [6, 8], "boil": 6, "hopelessli": 6, "checksynthord": 6, "random": 6, "deduc": [6, 7, 9], "outparam": 6, "trigger": [6, 8], "retri": 6, "monoidhomclass\u2082": 6, "promis": [6, 8, 9], "map_inv_of_inv": 6, "got": 6, "presenc": 6, "layer": [6, 9], "dfunlik": 6, "dfun": 6, "monoidhomclass": 6, "monoidhomclass\u2083": 6, "coe_inject": 6, "stop": 6, "ringhomclass\u2083": 6, "ringhom": [6, 7], "algebrahom": 6, "ve": [6, 9], "primarili": [6, 7, 9], "unbundl": 6, "orderpreshom": 6, "le_of_l": 6, "orderpresmonoidhom": 6, "orderpreshomclass": 6, "subgroup": 6, "subr": 6, "reus": 6, "led": 6, "descend": [6, 7], "break": 6, "barrier": 6, "setlik": 6, "wrap": [6, 9], "submonoid\u2081": 6, "submonoid": [6, 7], "mul_mem": [6, 7], "one_mem": [6, 7], "tackl": 6, "setco": 6, "submonoid\u2081monoid": 6, "destructur": 6, "binder": 6, "submonoidclass\u2081": 6, "subgroup\u2081": 6, "subgroupclass\u2081": 6, "subobject": 6, "s\u2081": 6, "s\u2082": 6, "shame": 6, "across": 6, "weird": [6, 9], "distract": 6, "emphas": [6, 7], "anecdot": 6, "devic": 6, "hasquoti": 6, "regular": [6, 9], "ascii": 6, "setoid": [6, 7], "commmonoid": 6, "iseqv": 6, "hw": 6, "quotientmonoid": 6, "map\u2082": 6, "treatment": 7, "constantli": 7, "review": [7, 9], "contort": 7, "verbatim": 7, "safer": 7, "friendli": 7, "proceed": 7, "mostli": 7, "comm": 7, "addcommmonoid": [7, 8], "monoidhom": 7, "addmonoidhom": 7, "packag": [7, 8], "unfortun": 7, "consequ": 7, "comp": [7, 8, 9], "map_inv": 7, "enforc": 7, "sent": [7, 9], "mulequiv": 7, "addequiv": 7, "ulequiv": 7, "projector": 7, "ofbiject": [7, 8], "closur": [7, 8, 9], "inv_mem": 7, "issubgroup": 7, "addsubgroup": 7, "add_mem": [7, 8], "zero_mem": [7, 8], "neg_mem": 7, "inferinst": [7, 8], "benefit": [7, 8], "amount": [7, 8], "sup_eq_closur": 7, "mem_bot": [7, 8], "ambient": 7, "ty": 7, "comap": [7, 8, 9], "pushforward": [7, 9], "mem_map": [7, 8], "mem_comap": [7, 8], "kernel": [7, 8], "ker": [7, 8], "mem_ker": [7, 8], "mem_rang": 7, "\u03c6": [7, 8, 9], "hst": 7, "\u03c8": [7, 8], "homomorph": 7, "lagrang": 7, "sylow": 7, "corner": 7, "nonconstruct": 7, "card": 7, "index_mul_card": 7, "hdvd": 7, "exists_subgroup_card_pow_prim": 7, "corollari": 7, "eq_bot_iff_card": 7, "eq_bot_iff_foral": 7, "card_eq_one_iff_exist": 7, "card_dvd_of_l": 7, "inf_bot_of_coprim": 7, "mathfrak": 7, "_n": 7, "cycl": 7, "iscycl": 7, "closure_iscycl": 7, "cyclic": 7, "freegroup": 7, "induct": [7, 8, 9, 13], "myelement": 7, "gave": [7, 9], "embodi": 7, "lift": [7, 8], "send": [7, 8, 11], "mymorph": 7, "cube": 7, "presentedgroup": 7, "normal": 7, "somehow": [7, 8], "creation": 7, "mygroup": 7, "feed": 7, "togroup": 7, "mymap": 7, "compat_mymap": 7, "mynewmorph": 7, "mulact": 7, "downsid": [7, 8], "setup": [7, 8], "synonym": 7, "groupact": 7, "addact": 7, "\u1d65": [7, 8], "affin": 7, "add_vadd": 7, "topermhom": 7, "caylei": [7, 8], "embed": 7, "cayleyisomorph": 7, "subgroupofmulact": 7, "partit": 7, "orbit": 7, "orbitrel": 7, "global": [7, 9], "\u03c9": 7, "selfequivsigmaorbit": 7, "fintyp": [7, 8, 9], "card_congr": 7, "card_sigma": 7, "furthermor": 7, "stabil": 7, "orbitequivquotientstabil": 7, "groupequivquotientprodsubgroup": 7, "conjugate_on": 7, "quotientgroup": 7, "clue": 7, "onto": [7, 8], "quotientkerequivrang": 7, "pullback": [7, 9], "quotientmulequivofeq": 7, "seri": 7, "card_po": 7, "index_eq_card": 7, "eq_of_mul_eq_mul_right": 7, "aux_card_eq": 7, "bijective_iff_injective_and_card": 7, "ker_eq_bot_iff": 7, "ker_restrict": 7, "iso\u2081": 7, "g\u2080": 7, "g\u2081": 7, "g\u2082": 7, "iso\u2082": 7, "prodcongr": 7, "finaliso": 7, "exot": [7, 9], "commsemir": [7, 8], "doubli": 7, "mislead": 7, "tradition": 7, "taught": 7, "promin": 7, "isunit": 7, "m\u02e3": 7, "mainli": 7, "mkofmuleqon": 7, "\u2124\u02e3": 7, "units_eq_one_or": 7, "r\u02e3": 7, "s\u02e3": 7, "ringequiv": 7, "toward": 7, "geometri": 7, "submodul": [7, 8], "eq_zero_iff_mem": 7, "mem_sup": [7, 8], "mul_le_left": 7, "mul_le_right": 7, "mul_le_inf": 7, "quotientmap": 7, "quotequivofeq": 7, "chines": 7, "\u03c0": [7, 8, 9, 10], "font": 7, "\u03b9": [7, 8, 9, 10, 11], "iscoprim": [7, 8], "quotientinfringequivpiquoti": 7, "zmod": 7, "pinot": 7, "prodequivpi": 7, "pi": [7, 8, 9], "ker_pi_quotient_mk": 7, "chinesemap": 7, "proven": [7, 8], "chinesemap_mk": 7, "famili": [7, 8, 9, 10], "injective_lift_iff": 7, "chinesemap_inj": 7, "maxim": 7, "iscoprime_iff_add": 7, "iscoprime_iff_exist": 7, "iscoprime_iff_sup_eq": 7, "iscoprime_iff_codisjoint": 7, "opportun": [7, 9], "mem_insert_of_mem": 7, "mem_insert_self": 7, "iscoprime_inf": 7, "simp_rw": 7, "iinf_insert": 7, "one_eq_top": 7, "eq_top_iff": 7, "chinesemap_surj": 7, "hi": 7, "mk_surject": 7, "\u1d9c": 7, "he": 7, "chineseiso": 7, "encod": [7, 11], "algebramap": 7, "alghom": 7, "\u2090": 7, "endomorph": [7, 13], "univari": 7, "indetermin": 7, "crucial": [7, 8, 9], "bodi": 7, "map_pow": 7, "coeff": 7, "degre": 7, "natdegre": 7, "withbot": 7, "absorb": 7, "formula": [7, 11], "nozerodivisor": 7, "degree_mul": 7, "hp": [7, 9], "hq": [7, 9], "natdegree_mul": 7, "natdegree_comp": 7, "evalu": [7, 8], "isroot": [7, 8], "vanish": [7, 8], "count": 7, "pain": 7, "multiset": 7, "roots_x_sub_c": 7, "aeval": [7, 8], "aroot": 7, "caveat": 7, "aroots_def": 7, "c_mul": 7, "c_neg": 7, "linear_combin": 7, "p_ne_zero": 7, "apply_fun": 7, "roots_mul": 7, "alembert": 7, "gauss": 7, "isalgclos": 7, "eval\u2082": 7, "ofrealhom": 7, "multivari": 7, "briefli": 7, "mvpolynomi": 7, "circl": 7, "circleequ": 7, "coordin": [7, 8], "9": 8, "eccentr": 8, "spell": [8, 9], "synthesi": 8, "smul_comm": 8, "advanc": 8, "medit": 8, "captur": 8, "ideal": 8, "\u2097": 8, "az": 8, "map_smul": [8, 10], "linearmap": 8, "\u03b8": 8, "action": 8, "attach": [8, 9], "wonder": 8, "etc": [8, 9], "lsmul": 8, "linearequiv": 8, "announc": 8, "binary_product": 8, "parallel": 8, "prodmap": 8, "aka": [8, 9], "coproduct": 8, "coprod": 8, "coprod_inl": 8, "coprod_inr": 8, "directsum": 8, "accid": 8, "assembl": [8, 9], "summand": 8, "tomodul": 8, "proj": 8, "lof": 8, "linearequivfunonfintyp": 8, "smul_mem": 8, "issubmodul": 8, "supersed": 8, "mem_preimag": 8, "span_union": 8, "iscompl": 8, "isintern": 8, "sup_eq_top": 8, "inf_eq_bot": 8, "submodule_isup_eq_top": 8, "pairwis": [8, 11], "hij": 8, "submodule_independ": 8, "pairwisedisjoint": 8, "eq_bot": 8, "isinternal_submodule_iff_independent_and_isup_eq_top": 8, "extern": 8, "coelinearmap": 8, "span_l": 8, "galoisinsert": 8, "gi": 8, "span_induct": 8, "stabl": 8, "span_eq": 8, "awkward": 8, "contributor": 8, "range_eq_map": 8, "comap_bot": 8, "flavor": 8, "elabor": [8, 9], "ker_eq_bot": 8, "range_eq_top": 8, "mem_map_of_mem": 8, "mkq": 8, "liftq": 8, "ker_mkq": 8, "range_mkq": 8, "h\u03c6": 8, "mapq": 8, "quotkerequivrang": 8, "comapmkqreliso": 8, "map_comap_eq": 8, "comap_map_eq": 8, "eigenvalu": 8, "eigenvector": 8, "mul_eq_comp": 8, "aeval_x": 8, "pq": 8, "eq_bot_iff": 8, "mem_inf": 8, "add_mem_sup": 8, "mul_appli": 8, "ker_le_ker_comp": 8, "eigenspac": 8, "aid": 8, "haseigenvector": 8, "eigenspace_def": 8, "haseigenvalu": 8, "exists_haseigenvector": 8, "hv": 8, "haseigenvalue_of_haseigenvector": 8, "minim": 8, "minpoli": 8, "isroot_of_haseigenvalu": 8, "finitedimension": [8, 10, 11], "haseigenvalue_iff_isroot": 8, "hamilton": 8, "charpoli": 8, "aeval_self_charpoli": 8, "sage": 8, "arrai": 8, "virtual": 8, "machin": 8, "matrix": 8, "row": 8, "column": 8, "resp": 8, "vecmul": 8, "mulvec": 8, "size": 8, "col": 8, "transpos": 8, "11": [8, 10], "\u1d40": 8, "det": [8, 11], "consider": 8, "trust": 8, "counter": 8, "adjug": 8, "cramer": 8, "inv_def": 8, "inv_mul_of_invert": 8, "invertibleofisunitdet": 8, "one_fin_two": 8, "adjac": 8, "meaning": 8, "fin_cas": 8, "lose": 8, "secretli": 8, "vandermond": 8, "linearli": 8, "repr": 8, "tortuou": 8, "useless": 8, "b_indep": 8, "linearindepend": 8, "b_span": 8, "mk_appli": 8, "finsupp": 8, "basissingleon": 8, "unneed": 8, "basisfun": 8, "sum_repr": 8, "account": 8, "linearcombin": 8, "linearcombination_apply_of_mem_support": 8, "linearcombination_repr": 8, "despit": 8, "constr": 8, "constr_basi": 8, "characterist": 8, "identif": 8, "tomatrix": 8, "tomatrix_mulvec_repr": 8, "shouldn": [8, 9], "tomatrix_comp": 8, "id_comp": 8, "comp_id": 8, "tomatrix_id": 8, "det_mul": 8, "det_on": 8, "dimension": [8, 10, 11], "finrank": 8, "finrank_fin_fun": 8, "finrank_self": 8, "finrank_real_complex": 8, "finrank_pos_iff": 8, "fine": 8, "of_fintype_basi": 8, "fintypebasisindex": 8, "finrank_sup_add_finrank_inf_eq": 8, "finrank_l": 8, "earli": 8, "rank": 8, "russel": 8, "paradox": [8, 9], "zeroth": 8, "u_n": 8, "u_2": 8, "mk_eq_mk_of_basi": 8, "finrank_eq_rank": 8, "calculu": [9, 11, 13], "quantiti": 9, "begun": 9, "x\u2080": [9, 10], "convention": 9, "eight": 9, "varieti": 9, "wish": 9, "64": 9, "y\u2080": 9, "z\u2080": 9, "paragraph": 9, "512": 9, "bourbaki": 9, "dualli": 9, "neighborhood": 9, "attop": [9, 11], "\ud835\udcdd": [9, 10, 11], "\ud835\udce4": 9, "entourag": 9, "\u03bc": [9, 11], "ae": [9, 11], "univ_set": 9, "sets_of_superset": 9, "inter_set": 9, "blur": 9, "princip": 9, "\ud835\udcdf": 9, "x_0": 9, "ioo": [9, 10], "tendsto\u2081": 9, "tendsto": [9, 11], "lim_": 9, "abstractli": 9, "salient": 9, "f_": 9, "tendsto\u2082": 9, "via": 9, "leverag": 9, "map_mono": 9, "map_map": 9, "shot": 9, "map_le_iff_le_comap": 9, "contravari": 9, "comap_comap": 9, "plane": 9, "\u02e2": 9, "nhds_prod_eq": 9, "aforement": 9, "le_inf_iff": 9, "prohibit": 9, "precondit": 9, "nebot": 9, "tour": [9, 10], "claim": 9, "recaptur": 9, "superfici": 9, "stronger": 9, "flexibl": 9, "hasbasi": 9, "nhds_basis_ioo_po": 9, "tendsto_iff": 9, "reformul": 9, "ici": 9, "attop_basi": 9, "knew": 9, "n_p": 9, "n_q": 9, "tiresom": 9, "\u1da0": [9, 10, 11], "superscript": 9, "eventuallyeq": 9, "tendsto_congr": 9, "of_foral": 9, "mono": 9, "item": 9, "filter_upward": 9, "hr": 9, "occasion": 9, "frequent": 9, "sophist": 9, "mem_closure_of_tendsto": 9, "clusterpt": 9, "mem_closure_iff_clusterpt": 9, "le_principal_iff": 9, "nebot_of_l": 9, "hux": 9, "hum": 9, "dist_eq_zero": 9, "emetricspac": 9, "pseudometricspac": 9, "pseudoemetricspac": 9, "journei": 9, "recast": 9, "tendsto_attop": 9, "continuous_iff": 9, "devot": 9, "uncurri": 9, "slow": 9, "continuous_fst": 9, "prod_mk": 9, "continuous_snd": 9, "continuous_dist": 9, "clunki": 9, "heavili": 9, "prod_map": 9, "sad": 9, "border": 9, "obfusc": 9, "continuous_pow": 9, "continuousat": [9, 11], "continuousat_iff": 9, "geometr": 9, "closedbal": 9, "sign": 9, "radiu": 9, "mem_ball_self": 9, "mem_closedball_self": 9, "isopen": 9, "isopen_iff": 9, "Their": [9, 10], "isclos": [9, 10], "s\u1d9c": [9, 11], "isopen_compl_iff": 9, "hu": [9, 10], "mem_of_tendsto": 9, "mem_closure_iff": 9, "mem_closure_iff_seq_limit": 9, "nhds_basis_bal": 9, "nhds_basis_closedbal": 9, "mem_iff": 9, "segment": [9, 11], "somewher": 9, "continuouson": [9, 10], "minimum": 9, "iscompact": 9, "icc": [9, 10], "iscompact_icc": 9, "strictmono": 9, "tendsto_subseq": 9, "exists_isminon": 9, "exists_ismaxon": 9, "compactspac": 9, "iscompact_univ": 9, "cauchi": 9, "uniformcontinu": 9, "uniformcontinuous_iff": 9, "clearli": 9, "isclosed_l": [9, 10], "eq_empty_or_nonempti": 9, "attain": 9, "cauchyseq": 9, "cauchyseq_iff": 9, "completespac": [9, 10, 11], "cauchyseq_tendsto_of_complet": 9, "criterion": 9, "tendsto_pow_attop_nhds_zero_of_lt_on": 9, "dist_le_range_sum_dist": 9, "cauchyseq_of_le_geometric_two": 9, "\u03b5_po": [9, 10], "le_iff_exists_add": 9, "boss": 9, "bair": [9, 10], "exclam": 9, "rec_on": 9, "ho": 9, "hd": 9, "dens": 9, "densiti": 9, "\u03b4po": 9, "hpo": 9, "hball": 9, "mem_closure_iff_nhds_basi": 9, "recon": 9, "rpo": 9, "rb": 9, "incl": 9, "cdist": 9, "ylim": 9, "yball": 9, "categor": 9, "topologicalspac": [9, 10], "isopen_univ": 9, "isopen_empti": 9, "isopen_iunion": 9, "isopen_iinter_of_finit": 9, "continuous_def": 9, "filteri": 9, "mem_nhds_iff": 9, "digress": 9, "pure_le_nhd": 9, "self_of_nhd": 9, "eventually_eventually_nhd": 9, "mkofnhd": 9, "nhds_mkofnhd": 9, "functori": 9, "induc": 9, "sensibl": 9, "uncount": 9, "relatedli": 9, "coinduc": 9, "t_x": 9, "t_y": 9, "coinduced_le_iff_le_induc": 9, "covari": 9, "coinduced_compos": 9, "induced_compos": 9, "focus": 9, "nhd": 9, "recov": 9, "continuous_iff_coinduced_l": 9, "g_": 9, "t_z": 9, "wasn": 9, "t_": 9, "x_i": 9, "price": 9, "patholog": 9, "t2space": 9, "hausdorff": 9, "t3space": 9, "regularspac": 9, "tendsto_nhds_uniqu": 9, "closed_nhds_basi": 9, "nhds_basis_open": 9, "t_3": 9, "denseinduc": 9, "continuousat_extend": 9, "funni": 9, "_in": 9, "nhds_induc": 9, "fortiori": 9, "f_cont": 9, "tendsto_right_iff": 9, "firstcountabletopolog": 9, "cluster": 9, "hfx": 9, "push_pul": 9, "of_map": 9, "f_ne": 9, "f_le": 9, "map_eq": 9, "hne": 9, "hle": 9, "huo": 9, "hsu": 9, "elim_finite_subcov": 9, "introductori": 10, "hasderivat": [10, 11], "hasderivat_sin": 10, "differentiableat": 10, "inconveni": 10, "deriv_zero_of_not_differentiableat": 10, "deriv_add": 10, "islocalmin": 10, "deriv_eq_zero": 10, "roll": 10, "weirder": 10, "hab": 10, "hfc": 10, "hfi": 10, "exists_deriv_eq_zero": 10, "differentiableon": 10, "exists_deriv_eq_slop": 10, "normedaddcommgroup": [10, 11], "norm_add_l": 10, "infer_inst": [10, 11], "normedspac": [10, 11], "normedaddgroup": 10, "stipul": 10, "norm_smul": 10, "banach": [10, 11], "\ud835\udd5c": [10, 11], "nontriviallynormedfield": [10, 11], "normedfield": 10, "exists_one_lt_norm": 10, "continuouslinearmap": 10, "cont": 10, "le_opnorm": 10, "hmp": 10, "hm": 10, "opnorm_le_bound": 10, "steinhau": 10, "bounded": 10, "uniformli": 10, "nonempty_interior_of_iunion_of_clos": 10, "continuous_linear_map": 10, "opnorm_le_of_shel": 10, "interior_subset": 10, "interior_iinter_subset": 10, "hc": 10, "h\u03b5": 10, "real_norm_l": 10, "\u03b5k_po": 10, "o": 10, "normedgroup": 10, "isbigowith": 10, "isbigowith_iff": 10, "isbigo_iff_isbigowith": 10, "islittleo_iff_forall_isbigowith": 10, "hasfderivat": 10, "fderiv": 10, "fr\u00e9chet": 10, "hasfderivatfilter_iff_islittleo": 10, "hff": 10, "iter": 10, "multilinear": 10, "withtop": 10, "infti": 10, "contdiff": 10, "iteratedfderiv": 10, "contdiff_iff_continuous_differenti": 10, "stricter": 10, "hasstrictfderivat": 10, "\ud835\udd42": 10, "rclike": 10, "contdiffat": 10, "localinvers": 10, "eventually_left_invers": 10, "eventually_right_invers": 10, "to_localinvers": 10, "hasfderivwithinat": [10, 11], "hasfderivatfilt": 10, "measuretheori": 11, "intervalintegr": 11, "integral_id": 11, "integral_one_div": 11, "differenti": [11, 13], "integral_hasstrictderivat_right": 11, "stronglymeasurableatfilt": 11, "volum": 11, "integral_eq_sub_of_hasderivat": 11, "convolut": 11, "bochner": 11, "lebesgu": 11, "measurablespac": 11, "countabl": 11, "measurableset": 11, "compl": 11, "iunion": 11, "iinter": 11, "measure_eq_iinf": 11, "measure_iunion_l": 11, "hmea": 11, "hdi": 11, "m_iunion": 11, "\u1d50": 11, "integral_add": 11, "ennreal": 11, "toreal": 11, "setintegral_const": 11, "domin": 11, "converg": [11, 13], "aestronglymeasur": 11, "hbound": 11, "hlim": 11, "tendsto_integral_of_dominated_converg": 11, "fubini": 11, "sigmafinit": 11, "\u03bd": 11, "integral_prod": 11, "bilinear": 11, "borelspac": 11, "isaddhaarmeasur": 11, "invari": 11, "mass": 11, "compact": 11, "h_inj": 11, "integral_image_eq_integral_abs_det_fderiv_smul": 11, "overview": 13, "schr\u00f6der": 13, "bernstein": 13, "irrat": 13, "dimens": 13}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"introduct": 0, "get": 0, "start": 0, "overview": 0, "basic": [1, 6], "calcul": 1, "prove": 1, "ident": 1, "algebra": [1, 5, 7, 8], "structur": [1, 5, 8], "us": 1, "theorem": [1, 3], "lemma": 1, "more": 1, "exampl": 1, "appli": 1, "rw": 1, "fact": 1, "about": 1, "logic": 2, "implic": 2, "univers": 2, "quantifi": 2, "The": [2, 3], "existenti": 2, "negat": 2, "conjunct": 2, "iff": 2, "disjunct": 2, "sequenc": 2, "converg": [2, 9], "set": [3, 8, 9], "function": [3, 9], "schr\u00f6der": 3, "bernstein": 3, "elementari": [4, 10, 11], "number": 4, "theori": [4, 11], "irrat": 4, "root": 4, "induct": 4, "recurs": 4, "infinit": 4, "mani": 4, "prime": 4, "defin": 5, "build": 5, "gaussian": 5, "integ": 5, "hierarchi": 6, "morphism": [6, 7], "sub": 6, "object": 6, "group": 7, "ring": 7, "monoid": 7, "subgroup": 7, "concret": 7, "action": 7, "quotient": [7, 8], "unit": 7, "subr": 7, "ideal": 7, "polynomi": 7, "linear": [8, 10], "vector": 8, "space": [8, 9, 10], "map": [8, 10], "sum": 8, "product": 8, "subspac": 8, "complet": [8, 9], "lattic": 8, "intern": 8, "direct": 8, "span": 8, "push": 8, "pull": 8, "endomorph": 8, "matric": 8, "base": 8, "dimens": 8, "topolog": 9, "filter": 9, "metric": 9, "continu": [9, 10], "ball": 9, "open": 9, "close": 9, "compact": 9, "uniformli": 9, "fundament": 9, "separ": 9, "countabl": 9, "differenti": 10, "calculu": 10, "norm": 10, "asymptot": 10, "comparison": 10, "integr": 11, "measur": 11, "index": 12, "mathemat": 13, "lean": 13}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 6, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx": 56}})