Theorems · Theorem · group theory
AddChar.doubleDualEmb_inj
∀ {α : Type u_1} [inst : AddCommGroup α] {a b : α} [Finite α], AddChar.doubleDualEmb a = AddChar.doubleDualEmb b ↔ a = b- Cited by
- 1 results in Mathlib
- Foundations
- Depth 243 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommGroupFinite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- AddCommGroupstatement and proof · cited by 12,871
- Complexstatement · cited by 5,565
- AddMonoidHomstatement · cited by 3,230
- Finitestatement and proof · cited by 3,029
- AddCharstatement · cited by 286
- AddChar.doubleDualEmbstatement · cited by 11
- AddChar.doubleDualEmb_injectiveproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- AddChar.doubleDualEmb_eq_zeroproof · cited by 1