ChargeUnit
📁 Source: PhysLean/Electromagnetism/Charge/ChargeUnit.lean
Statistics
| Metric | Count |
|---|---|
| 7 | |
| 14 | |
| Total | 21 |
ChargeUnit
Definitions
| Name | Category | Theorems |
|---|---|---|
coulombs 📖 | CompOp | |
elementaryCharge 📖 | CompOp | — |
instHDivNNReal 📖 | CompOp | |
instInhabited 📖 | CompOp | — |
scale 📖 | CompOp | |
val 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
div_eq_val 📖 | mathematical | — | ChargeUnitinstHDivNNRealvalval_pos | — | — |
div_mul_div_coe 📖 | mathematical | — | ChargeUnitinstHDivNNReal | — | — |
div_neq_zero 📖 | mathematical | — | ChargeUnitinstHDivNNReal | — | val_posdiv_eq_val |
div_pos 📖 | mathematical | — | ChargeUnitinstHDivNNReal | — | div_neq_zero |
div_self 📖 | mathematical | — | ChargeUnitinstHDivNNReal | — | val_posval_neq_zero |
div_symm 📖 | mathematical | — | ChargeUnitinstHDivNNReal | — | val_posdiv_eq_val |
property 📖 | mathematical | — | val | — | — |
scale_div_scale 📖 | mathematical | — | ChargeUnitinstHDivNNRealscale | — | — |
scale_div_self 📖 | mathematical | — | ChargeUnitinstHDivNNRealscale | — | val_pos |
scale_one 📖 | mathematical | — | scale | — | — |
scale_scale 📖 | mathematical | — | scale | — | — |
self_div_scale 📖 | mathematical | — | ChargeUnitinstHDivNNRealscale | — | val_pos |
val_neq_zero 📖 | — | — | — | — | property |
val_pos 📖 | mathematical | — | val | — | property |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
ChargeUnit 📖 | CompData |
---