Theorems · Theorem · group theory
Units.mk0.congr_simp
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a a_1 : G₀) (e_a : a = a_1) (ha : a ≠ 0), Units.mk0 a ha = Units.mk0 a_1 ⋯- Cited by
- 17 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Unitsstatement · cited by 2,804
- GroupWithZerostatement and proof · cited by 691
- Units.mk0statement and proof · cited by 181
Cited by17
Results whose statement or proof uses this declaration.
- Valuation.subgroups_basisproof · cited by 5
- ValuativeRel.ValueGroupWithZero.embed_strictMonoproof · cited by 4
- MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mkproof · cited by 3
- Units.mk0_prodproof · cited by 2
- Valuation.IsEquiv.uniformContinuous_equivproof · cited by 2
- Valued.continuous_valuation_of_surjectiveproof · cited by 2
- Polynomial.sub_one_pow_totient_lt_cyclotomic_evalproof · cited by 2
- Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integerproof · cited by 2
- Valuation.nonempty_rankOne_iff_mulArchimedeanproof · cited by 1
- Valuation.IsEquiv.uniformContinuous_equiv_symmproof · cited by 1
- Valuation.IsUniformizer.zpowers_eq_valueGroupproof · cited by 1
- Polynomial.cyclotomic_eval_lt_add_one_pow_totientproof · cited by 1