How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
and are subgroups of
Statement
For every group , element , and subgroup , both the centralizer and the normalizer are subgroups of .
Facts & Assumptions
Given: A group , an element , and a subgroup .
The centralizer is (The conjugacy class and centralizer of an element).
The normalizer is (The normalizer of a subgroup).
A nonempty subset is a subgroup if whenever (One-step subgroup test: a nonempty is a subgroup iff for all ; the identity and the inverses of are then those of ).
Proof
The identity commutes with . If , then commutes with , and hence ; [L3] gives .
The identity normalizes . If , then , and therefore .
Applying [L3] to step 1.2 gives , so both asserted sets are subgroups.
Depends on
- The conjugacy class $\operatorname{Cl}_G(x)$ and centralizer $C_G(x)$ of an element
- The normalizer $N_G(H)=\{g\in G:gHg^{-1}=H\}$ of a subgroup
- One-step subgroup test: a nonempty $H \subseteq G$ is a subgroup iff $gh^{-1} \in H$ for all $g, h \in H$; the identity and the inverses of $H$ are then those of $G$
Used by
- G/C_G(x)toCl_G(x) is a bijection, so |Cl_G(x)|=[G:C_G(x)] whenever these cardinalities are finite Theorem
- The conjugates of a proper subgroup do not cover a finite group Theorem
- The conjugates of H are in bijection with G/N_G(H) and, for finite G, number [G:N_G(H)] Theorem
Cited to discharge well-definedness by The conjugacy class Cl_G(x) and centralizer C_G(x) of an element and The normalizer N_G(H)={g∈ G:gHg⁻¹=H} of a subgroup.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 15 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- P. Brosnan, Undergraduate Algebra Notes, 3.14: G-Sets (standard reference, not scraped)