Diff — 0
Revision #965 → #1680 · back to history
modifiedZero as empty quantityb222d50591fb
| Field | From #965 | To #1680 |
|---|
| mathlib.module | — | Mathlib.Algebra.Group.Defs |
modifiedZero smallest nonnegative integer7df67cb3f396
| Field | From #965 | To #1680 |
|---|
| mathlib.module | — | Mathlib.Data.Nat.Defs |
modifiedZero is evend33caeab2551
| Field | From #965 | To #1680 |
|---|
| note | `Even.zero : Even (0 : α)` states that zero is even. | `Even.zero : Even (0 : α)` (auto-generated from `IsSquare.one` via `@[to_additive]`) states that zero is even. |
modifiedZero as cardinality of empty setcc781cca71e9
| Field | From #965 | To #1680 |
|---|
| mathlib.module | Mathlib.SetTheory.Cardinal.Basic | Mathlib.SetTheory.Cardinal.Defs |
| note | `Cardinal.mk_eq_zero` gives `#(empty) = 0` (also `Set.ncard_empty`, `Finset.card_empty`). | `Cardinal.mk_eq_zero : [IsEmpty α] → #α = 0` (also `Set.ncard_empty`, `Finset.card_empty`). |
modifiedZero as lowest ordinalb763f4f7eec5
| Field | From #965 | To #1680 |
|---|
| note | Ordinals carry `OrderBot` with `bot_eq_zero`, so `0` is the least ordinal. | `Ordinal.bot_eq_zero : (⊥ : Ordinal) = 0` shows `0` is the least ordinal. |
modifiedZero element941093b3506f
| Field | From #965 | To #1680 |
|---|
| mathlib.module | — | Mathlib.Algebra.Group.Defs |
addedZero divided by nonzero87dd70c80f51
addedZero to a positive power592cd8610f7a
addedZero morphismd5015373a8bb
addedZero is an integer multiple of any integerc6a2a1c555b0