Comments (2)
Thanks for the input! In Lean's axiomatization of Ring
(and in even more basic structures), the minus symbol and negation symbol are declared independently and the axioms imply a - b = a +-b
. That gives users more flexibility in defining particular instances. For example, one can define subtraction and negation on the reals independently (e.g. in terms of Cauchy sequences) and then prove that they agree.
If the axioms fixed the definition of subtraction, we could have trouble whenever someone declared an instance that already has a subtraction defined. On the other hand, including subtraction in the structure and axiomatizing its behavior means that we can use the same generic theorems no matter how subtraction is defined in particular instances.
This is a common theme in Mathlib; see the discussion of diamond problems in Section 7.1. We plan to revise MIL soon and will clarify this.
from mathematics_in_lean_source.
Thanks a lot for the answer! I'm still a bit new to Lean to understand it perfectly but I kind of see the idea!
from mathematics_in_lean_source.
Related Issues (20)
- example "evens โช odds = univ" fails HOT 3
- FunLike update
- Lack of Introduction for Many Facts Used in the Tutorial HOT 2
- Specify explicit version of mathlib in lakefile HOT 1
- Consider adding the failed example relevant to the bad diamond issue in Chapter7 ยง1
- `tauto!`
- `refine'`
- Minor typo at S02_Overview.lean
- Simp and let
- Replace induction' with induction
- C04/S02: Possible redundant exercise
- Exercise for S2.5 requires setting implicit arguments HOT 6
- Explain `convert ... using` in C03S06
- bug in 8.1.4. Concrete groups? HOT 1
- This menu option does not appear in VS code extension now. HOT 1
- "rintros" used in text HOT 1
- Explanation about Inverse function in Chapter 4
- `dif_pos` versus `if_pos` in Chapter 4 HOT 1
- `cases` versus `cases'` HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. ๐๐๐
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google โค๏ธ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from mathematics_in_lean_source.