Documentation Verification Report

Elems

📁 Source: PhysLean/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean

Statistics

Metric	Count
Definitions `elemsNoExotics`, `elemsNoExotics`	2
Theorems `card_le_six_mem_elemsNoExotics`, `elemsNoExotics_card`, `elemsNoExotics_nodup`, `hasNoZero_of_mem_elemsNoExotics`, `map_sum_add_of_mem_powerset_elemsNoExotics`, `noExotics_of_mem_elemsNoExotics`, `sum_of_mem_elemsNoExotics`, `toFinset_card_le_four_mem_elemsNoExotics`, `elemsNoExotics_card`, `elemsNoExotics_nodup`, `hasNoZero_of_mem_elemsNoExotics`, `noExotics_of_mem_elemsNoExotics`, `sum_of_mem_elemsNoExotics`, `toFinset_card_le_three_mem_elemsNoExotics`	14
Total	16

FTheory.SU5.FluxesFive

Definitions

Name	Category	Theorems
`elemsNoExotics` 📖	CompOp	5 math math: `noExotics_iff_mem_elemsNoExotics`, `elemsNoExotics_card`, `mem_elemsNoExotics_of_noExotics`, `FTheory.SU5.FiveQuanta.mem_liftCharge_iff`, `elemsNoExotics_nodup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_six_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `elemsNoExotics`	`FTheory.SU5.Fluxes`	—	—
`elemsNoExotics_card` 📖	mathematical	—	`FTheory.SU5.FluxesFive` `elemsNoExotics`	—	—
`elemsNoExotics_nodup` 📖	mathematical	—	`FTheory.SU5.FluxesFive` `elemsNoExotics`	—	—
`hasNoZero_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `elemsNoExotics`	`HasNoZero`	—	—
`map_sum_add_of_mem_powerset_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `elemsNoExotics` `FTheory.SU5.Fluxes`	`FTheory.SU5.Fluxes.instAdd` `FTheory.SU5.Fluxes.instAddCommMonoid` `FTheory.SU5.Fluxes.M` `FTheory.SU5.Fluxes.N`	—	—
`noExotics_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `elemsNoExotics`	`NoExotics`	—	—
`sum_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `elemsNoExotics`	`FTheory.SU5.Fluxes` `FTheory.SU5.Fluxes.instAddCommMonoid`	—	—
`toFinset_card_le_four_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesFive` `elemsNoExotics`	`FTheory.SU5.Fluxes` `FTheory.SU5.instDecidableEqFluxes`	—	—

FTheory.SU5.FluxesTen

Definitions

Name	Category	Theorems
`elemsNoExotics` 📖	CompOp	5 math math: `elemsNoExotics_card`, `FTheory.SU5.TenQuanta.mem_liftCharge_iff`, `mem_elemsNoExotics_of_noExotics`, `noExotics_iff_mem_elemsNoExotics`, `elemsNoExotics_nodup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elemsNoExotics_card` 📖	mathematical	—	`FTheory.SU5.FluxesTen` `elemsNoExotics`	—	—
`elemsNoExotics_nodup` 📖	mathematical	—	`FTheory.SU5.FluxesTen` `elemsNoExotics`	—	—
`hasNoZero_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `elemsNoExotics`	`HasNoZero`	—	—
`noExotics_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `elemsNoExotics`	`NoExotics`	—	—
`sum_of_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `elemsNoExotics`	`FTheory.SU5.Fluxes` `FTheory.SU5.Fluxes.instAddCommMonoid`	—	—
`toFinset_card_le_three_mem_elemsNoExotics` 📖	mathematical	`FTheory.SU5.FluxesTen` `elemsNoExotics`	`FTheory.SU5.Fluxes` `FTheory.SU5.instDecidableEqFluxes`	—	—

---

← Back to Index